diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-23 00:58:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-23 00:58:17 +0200 |
| commit | 47fbb3a74b9bd52b19e63e695fb1902ed345488e (patch) | |
| tree | 1fa04bcc4d12d45b5682cb87447b289ced3b6a6a /tactics | |
| parent | a67cc6941434124465f20b14a1256f2ede31a60e (diff) | |
Tactics.unify in the new monad.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 10 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
3 files changed, 9 insertions, 7 deletions
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 |