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 +++++---- plugins/ltac/rewrite.ml | 37 +++++++++++++++++++++---------------- plugins/ltac/tacsubst.ml | 3 +-- plugins/ltac/tauto.ml | 4 +--- 4 files changed, 28 insertions(+), 25 deletions(-) (limited to 'plugins/ltac') 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 diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 966b11d0e..dadcfb9f2 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -751,17 +751,23 @@ let default_flags = { under_lambdas = true; on_morphisms = true; } let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None -let make_eq () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) -let make_eq_refl () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ())) +let new_global (evars, cstrs) gr = + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr + in (Sigma.to_evar_map sigma, cstrs), c -let get_rew_prf r = match r.rew_prf with - | RewPrf (rel, prf) -> rel, prf +let make_eq sigma = + new_global sigma (Coqlib.build_coq_eq ()) +let make_eq_refl sigma = + new_global sigma (Coqlib.build_coq_eq_refl ()) + +let get_rew_prf evars r = match r.rew_prf with + | RewPrf (rel, prf) -> evars, (rel, prf) | RewCast c -> - let rel = mkApp (make_eq (), [| r.rew_car |]) in - rel, mkCast (mkApp (make_eq_refl (), [| r.rew_car; r.rew_from |]), - c, mkApp (rel, [| r.rew_from; r.rew_to |])) + let evars, eq = make_eq evars in + let evars, eq_refl = make_eq_refl evars in + let rel = mkApp (eq, [| r.rew_car |]) in + evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]), + c, mkApp (rel, [| r.rew_from; r.rew_to |]))) let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation @@ -827,7 +833,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev env evars carrier relation x in [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs' | Some r -> - [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, + let evars, proof = get_rew_prf evars r in + [ snd proof; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs') | None -> if not (Option.is_empty y) then @@ -847,7 +854,8 @@ let apply_constraint env avoid car rel prf cstr res = | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res let coerce env avoid cstr res = - let rel, prf = get_rew_prf res in + let evars, (rel, prf) = get_rew_prf res.rew_evars res in + let res = { res with rew_evars = evars } in apply_constraint env avoid res.rew_car rel prf cstr res let apply_rule unify loccs : int pure_strategy = @@ -868,8 +876,7 @@ let apply_rule unify loccs : int pure_strategy = else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in - let rel, prf = get_rew_prf res in - let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in + let res = Success (coerce env unfresh cstr res) in (occ, res) } @@ -1231,9 +1238,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in let res = match res with - | Success r -> - let rel, prf = get_rew_prf r in - Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r) + | Success r -> Success (coerce env unfresh (prop,cstr) r) | Fail | Identity -> res in state, res | _ -> state, Fail diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 4390ff08b..8cbe9c690 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -14,7 +14,6 @@ open Stdarg open Tacarg open Misctypes open Globnames -open Term open Genredexpr open Patternops @@ -91,7 +90,7 @@ open Printer let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in - if not (eq_constr (Universes.constr_of_global ref') t') then + if not (is_global ref' t') then Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4ec111e01..d8e21d81d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -220,9 +220,7 @@ let apply_nnpp _ ist = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> try - let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in - let nnpp = EConstr.of_constr nnpp in - apply nnpp + Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply with Not_found -> tclFAIL 0 (Pp.mt ()) end -- cgit v1.2.3