aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/gen_principle.ml10
-rw-r--r--plugins/funind/indfun_common.ml1
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/ltac/pptactic.ml8
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/taccoerce.ml1
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacexpr.ml4
-rw-r--r--plugins/ltac/tacexpr.mli4
-rw-r--r--plugins/ltac/tacintern.ml4
-rw-r--r--plugins/ltac/tacsubst.ml2
-rw-r--r--plugins/ltac/tauto.ml1
-rw-r--r--plugins/omega/coq_omega.ml3
-rw-r--r--plugins/ssr/ssrequality.ml6
15 files changed, 28 insertions, 24 deletions
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. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:38:17 +0000