From 22014c3fd400446556d3c2d7548d4638a7ed96ee Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 29 May 2017 17:39:03 +0200 Subject: Ltac cleanup: no more constr_of_global calls --- plugins/ltac/extratactics.ml4 | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'plugins/ltac/extratactics.ml4') diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index d68139a4b..2f2a5cdb0 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -306,7 +306,8 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let p = EConstr.of_constr @@ Universes.constr_of_global p in + let sigma, p = Evd.fresh_global env sigma p in + let p = EConstr.of_constr p in let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in @@ -735,7 +736,6 @@ let rewrite_except h = let refl_equal = let coq_base_constant s = - Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in function () -> (coq_base_constant "eq_refl") @@ -747,8 +747,9 @@ let refl_equal = let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in - Tacticals.New.tclTHENLIST - [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))]; + Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> + Tacticals.New.tclTHENLIST + [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in -- cgit v1.2.3