From c92bb5b1da8223d61e0ac63a4ebd4a54f46d4670 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 23 Jun 2014 17:22:56 +0200
Subject: Clenvtac.unify is in the new monad.

---
 proofs/clenvtac.ml  | 19 ++++++++++---------
 proofs/clenvtac.mli |  2 +-
 2 files changed, 11 insertions(+), 10 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 6873bbb112..941d789dd5 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 173eb32e31..3cfe1f3155 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
 
-- 
cgit v1.2.3