diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 27 |
1 files changed, 14 insertions, 13 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 891e2dba..cab74968 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -262,16 +262,15 @@ TACTIC EXTEND rewrite_star (* Hint Rewrite *) let add_rewrite_hint bases ort t lcsr = - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in let poly = Flags.is_universe_polymorphism () in let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = - if poly then - Evd.evar_universe_context_set ctx - else - let cstrs = Evd.evar_universe_context_constraints ctx in - (Global.add_constraints cstrs; Univ.ContextSet.empty) + let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in + if poly then ctx + else (Global.push_context_set false ctx; Univ.ContextSet.empty) in Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in let eqs = List.map f lcsr in @@ -320,7 +319,7 @@ let project_hint pri l2r r = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in let ctx = Evd.universe_context_set sigma in - let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff l2r lc n bl = @@ -490,7 +489,9 @@ let inTransitivity : bool * constr -> obj = (* Main entry points *) let add_transitivity_lemma left lem = - let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in + let env = Global.env () in + let sigma = Evd.from_env env in + let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in add_anonymous_leaf (inTransitivity (left,lem')) (* Vernacular syntax *) @@ -704,7 +705,7 @@ let refl_equal = call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> - let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in + let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); Proofview.Goal.nf_enter begin fun gl -> @@ -750,12 +751,12 @@ let rec find_a_destructable_match t = let destauto t = try find_a_destructable_match t; - Proofview.tclZERO (UserError ("", str"No destructable match found")) + Tacticals.New.tclZEROMSG (str "No destructable match found") with Found tac -> tac let destauto_in id = Proofview.Goal.nf_enter begin fun gl -> - let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in + let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype @@ -772,7 +773,7 @@ END let eq_constr x y = Proofview.Goal.enter (fun gl -> let evd = Proofview.Goal.sigma gl in - if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT () + if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal")) TACTIC EXTEND constr_eq @@ -966,7 +967,7 @@ let guard tst = Proofview.tclUNIT () else let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in - Proofview.tclZERO (Errors.UserError("guard",msg)) + Tacticals.New.tclZEROMSG msg TACTIC EXTEND guard |