From 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 29 Oct 2020 13:59:45 +0100 Subject: Move evaluable_global_reference from Names to Tacred. It is the only place where it starts making sense in the whole codebase. It also fits nicely there since there are other functions manipulating this type in that module. In any case this type does not belong to the kernel. --- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/gen_principle.ml | 10 +++++----- plugins/funind/indfun_common.ml | 1 + plugins/funind/indfun_common.mli | 2 +- plugins/ltac/pptactic.ml | 8 ++++---- plugins/ltac/pptactic.mli | 2 +- plugins/ltac/taccoerce.ml | 1 + plugins/ltac/taccoerce.mli | 2 +- plugins/ltac/tacexpr.ml | 4 ++-- plugins/ltac/tacexpr.mli | 4 ++-- plugins/ltac/tacintern.ml | 4 ++-- plugins/ltac/tacsubst.ml | 2 +- plugins/ltac/tauto.ml | 1 + plugins/omega/coq_omega.ml | 3 ++- plugins/ssr/ssrequality.ml | 6 +++--- 15 files changed, 28 insertions(+), 24 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 73eb943418..67b6839b6e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1260,7 +1260,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalConstRef (fst fname) ) ] + , Tacred.EvalConstRef (fst fname) ) ] ; (let do_prove = build_proof interactive_proof (Array.to_list fnames) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 314c8abcaf..c344fdd611 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -917,13 +917,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic = tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(1)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(1)) ) ] ; tclMAP (fun id -> tclTRY (unfold_in_hyp [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(1)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(1)) ) ] (destVar sigma args.(1), Locus.InHyp))) (pf_ids_of_hyps g) ; intros_with_rewrite () ] @@ -936,13 +936,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic = tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(2)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(2)) ) ] ; tclMAP (fun id -> tclTRY (unfold_in_hyp [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(2)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(2)) ) ] (destVar sigma args.(2), Locus.InHyp))) (pf_ids_of_hyps g) ; intros_with_rewrite () ] @@ -1158,7 +1158,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : else unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalConstRef + , Tacred.EvalConstRef (fst (destConst (Proofview.Goal.sigma g) f)) ) ] in (* The proof of each branche itself *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6464556e4e..266345a324 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -418,6 +418,7 @@ let make_eq () = with _ -> assert false let evaluable_of_global_reference r = + let open Tacred in (* Tacred.evaluable_of_global_reference (Global.env ()) *) match r with | GlobRef.ConstRef sp -> EvalConstRef sp diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 7b7044fdaf..e25f413fe4 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -100,7 +100,7 @@ val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : - GlobRef.t -> Names.evaluable_global_reference + GlobRef.t -> Tacred.evaluable_global_reference val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index faad792ea9..6ebb01703f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -191,8 +191,8 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c let pr_evaluable_reference = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp) + | Tacred.EvalVarRef id -> pr_id id + | Tacred.EvalConstRef sp -> pr_global (GlobRef.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n @@ -381,8 +381,8 @@ let string_of_genarg_arg (ArgumentType arg) = str "<" ++ KerName.print kn ++ str ">" let pr_evaluable_reference_env env = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> + | Tacred.EvalVarRef id -> pr_id id + | Tacred.EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp) let pr_as_disjunctive_ipat prc ipatl = diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 79e0adf9f7..4f58eceb59 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -106,7 +106,7 @@ val pr_may_eval : val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t -val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t +val pr_evaluable_reference_env : env -> Tacred.evaluable_global_reference -> Pp.t val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9abdc2ddbe..5e88bf7c79 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -276,6 +276,7 @@ let coerce_to_closed_constr env v = c let coerce_to_evaluable_ref env sigma v = + let open Tacred in let fail () = raise (CannotCoerceTo "an evaluable reference") in let ev = match is_intro_pattern v with diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index b8592c5c76..8ca2510459 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -69,7 +69,7 @@ val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr val coerce_to_evaluable_ref : - Environ.env -> Evd.evar_map -> Value.t -> evaluable_global_reference + Environ.env -> Evd.evar_map -> Value.t -> Tacred.evaluable_global_reference val coerce_to_constr_list : Environ.env -> Value.t -> constr list diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 7b2c8e1d04..a880a3305e 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -270,7 +270,7 @@ constraint 'a = < type g_trm = Genintern.glob_constr_and_expr type g_pat = Genintern.glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var +type g_cst = Tacred.evaluable_global_reference Genredexpr.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -324,7 +324,7 @@ type raw_tactic_arg = type t_trm = EConstr.constr type t_pat = constr_pattern -type t_cst = evaluable_global_reference +type t_cst = Tacred.evaluable_global_reference type t_ref = ltac_constant located type t_nam = Id.t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 2382dcfbb9..3bb20b9d19 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -269,7 +269,7 @@ constraint 'a = < type g_trm = Genintern.glob_constr_and_expr type g_pat = Genintern.glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var +type g_cst = Tacred.evaluable_global_reference Genredexpr.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -323,7 +323,7 @@ type raw_tactic_arg = type t_trm = EConstr.constr type t_pat = constr_pattern -type t_cst = evaluable_global_reference +type t_cst = Tacred.evaluable_global_reference type t_ref = ltac_constant located type t_nam = Id.t diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 8bee7afa2c..ae7a10ce52 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -308,8 +308,8 @@ let short_name qid = else None let evalref_of_globref ?loc ?short = function - | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short) - | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short) + | GlobRef.ConstRef cst -> ArgArg (Tacred.EvalConstRef cst, short) + | GlobRef.VarRef id -> ArgArg (Tacred.EvalVarRef id, short) | r -> let tpe = match r with | GlobRef.IndRef _ -> "inductive" diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 90546ea939..6148f0d23f 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -89,7 +89,7 @@ let subst_global_reference subst = Locusops.or_var_map (subst_located (subst_global_reference subst)) let subst_evaluable subst = - let subst_eval_ref = subst_evaluable_reference subst in + let subst_eval_ref = Tacred.subst_evaluable_reference subst in Locusops.or_var_map (subst_and_short_name subst_eval_ref) let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index a7b571d3db..7d959aa788 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -189,6 +189,7 @@ let flatten_contravariant_disj _ ist = | _ -> fail let evalglobref_of_globref = + let open Tacred in function | GlobRef.VarRef v -> EvalVarRef v | GlobRef.ConstRef c -> EvalConstRef c diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4f7b3fbe74..9d92ffde74 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -354,8 +354,9 @@ let coq_True = gen_constant "core.True.type" let evaluable_ref_of_constr s c = let env = Global.env () in let evd = Evd.from_env env in + let open Tacred in match EConstr.kind evd (Lazy.force c) with - | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) -> + | Const (kn,u) when is_evaluable env (EvalConstRef kn) -> EvalConstRef kn | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant.")) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index fdfba48024..723c786b4f 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -223,11 +223,11 @@ let simplintac occ rdx sim = end let rec get_evalref env sigma c = match EConstr.kind sigma c with - | Var id -> EvalVarRef id - | Const (k,_) -> EvalConstRef k + | Var id -> Tacred.EvalVarRef id + | Const (k,_) -> Tacred.EvalConstRef k | App (c', _) -> get_evalref env sigma c' | Cast (c', _, _) -> get_evalref env sigma c' - | Proj(c,_) -> EvalConstRef(Projection.constant c) + | Proj(c,_) -> Tacred.EvalConstRef(Projection.constant c) | _ -> errorstrm Pp.(str "The term " ++ pr_econstr_pat (Global.env ()) sigma c ++ str " is not unfoldable") (* Strip a pattern generated by a prenex implicit to its constant. *) -- cgit v1.2.3