Clenvtac.unify is in the new monad.

4 files changed, 13 insertions, 12 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 6873bbb11..941d789dd 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -104,14 +104,15 @@ let fail_quick_unif_flags = {
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
-  let env = pf_env gls in
-  let evd = create_goal_evar_defs (project gls) in
-    try 
+let unify ?(flags=fail_quick_unif_flags) m =
+  Proofview.Goal.raw_enter begin fun gl ->
+    let env = Tacmach.New.pf_env gl in
+    let n = Tacmach.New.pf_nf_concl gl in
+    let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in
+    try
       let evd' = w_unify env evd CONV ~flags m n in
-	tclIDTAC {it = gls.it; sigma =  evd'; }
+      Proofview.V82.tclEVARS evd'
     with e when Errors.noncritical e ->
-      tclFAIL 0 (Errors.print e) gls
-
-let unify ?(flags=fail_quick_unif_flags) m gls =
-  let n = pf_concl gls in unifyTerms ~flags m n gls
+      (** This is Tacticals.tclFAIL *)
+      Proofview.tclZERO (FailError (0, lazy (Errors.print e)))
+  end
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 173eb32e3..3cfe1f315 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -13,7 +13,7 @@ open Tacexpr
 open Unification
 
 (** Tactics *)
-val unify : ?flags:unify_flags -> constr -> tactic
+val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
 val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic
 val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 31fbc0661..f11c027ad 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -98,7 +98,7 @@ let e_give_exact flags poly (c,clenv) gl =
     else c, gl
   in
   let t1 = pf_type_of gl c in
-    tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
+    tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
 
 let unify_e_resolve poly flags (c,clenv) gls =
   let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index bc3ad026c..98e7d3ff5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -34,7 +34,7 @@ let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_tr
 
 let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
   if occur_existential t1 || occur_existential t2 then
-     tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
+     tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
   else Proofview.V82.of_tactic (exact_check c) gl
 
 let assumption id = e_give_exact (mkVar id)