Merge pull request #501 from FStarLang/_nik_impure_spec_phase1_teq

impure spec elab should also use phase1 matcher

Author: nikswamy

src/checker/Pulse.Checker.ImpureSpec.fst

@@ -81,7 +81,7 @@ let prove_this (g: env) (goal: slprop) (ctxt: list slprop) : T.Tac (option (list
       match ctxt with
       | [] -> false
       | c::ctxt ->
-        if RU.teq_nosmt_force (elab_env g) goal c then
+        if RU.teq_nosmt_force_phase1 (elab_env g) goal c then
           true
         else
           try_match ctxt