From 47fbb3a74b9bd52b19e63e695fb1902ed345488e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 23 Aug 2014 00:58:17 +0200
Subject: Tactics.unify in the new monad.

---
 tactics/eauto.ml4   |  4 ++--
 tactics/tactics.ml  | 10 ++++++----
 tactics/tactics.mli |  2 +-
 3 files changed, 9 insertions(+), 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index a4babd276..2dabe9011 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -593,7 +593,7 @@ TACTIC EXTEND autounfoldify
 END
 
 TACTIC EXTEND unify
-| ["unify" constr(x) constr(y) ] -> [ Proofview.V82.tactic (unify x y) ]
+| ["unify" constr(x) constr(y) ] -> [ unify x y ]
 | ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
     let table = try Some (searchtable_map base) with Not_found -> None in
     match table with
@@ -602,7 +602,7 @@ TACTIC EXTEND unify
       Proofview.tclZERO (UserError ("", msg))
     | Some t ->
       let state = Hint_db.transparent_state t in
-      Proofview.V82.tactic (unify ~state x y)
+      unify ~state x y
   ]
 END
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7a8bb36b9..5c76ce776 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4004,7 +4004,8 @@ let admit_as_an_axiom =
 (*     gl *)
 (* >>>>>>> .merge_file_iUuzZK *)
 
-let unify ?(state=full_transparent_state) x y gl =
+let unify ?(state=full_transparent_state) x y =
+  Proofview.Goal.enter begin fun gl ->
   try
     let flags =
       {(default_unify_flags ()) with
@@ -4013,9 +4014,10 @@ let unify ?(state=full_transparent_state) x y gl =
        modulo_delta_in_merge = Some state;
        modulo_conv_on_closed_terms = Some state}
     in
-    let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
-    in tclEVARS evd gl
-  with e when Errors.noncritical e -> tclFAIL 0 (str"Not unifiable") gl
+    let evd = w_unify (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) Reduction.CONV ~flags x y
+    in Proofview.V82.tclEVARS evd
+  with e when Errors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Not unifiable")
+  end
 
 module Simple = struct
   (** Simplified version of some of the above tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e5ba7f14c..d7a88787b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -387,7 +387,7 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 
 (** {6 Other tactics. } *)
 
-val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
+val unify           : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
 
 val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
-- 
cgit v1.2.3