aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--plugins/firstorder/rules.ml7
-rw-r--r--plugins/funind/functional_principles_proofs.ml8
-rw-r--r--plugins/funind/indfun_common.ml8
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--plugins/ltac/tacenv.ml7
-rw-r--r--plugins/ltac/tacintern.ml13
-rw-r--r--plugins/ltac/tacinterp.ml9
-rw-r--r--plugins/nsatz/nsatz.ml4
-rw-r--r--plugins/omega/coq_omega.ml3
-rw-r--r--plugins/rtauto/refl_tauto.ml8
-rw-r--r--plugins/setoid_ring/newring.ml6
-rw-r--r--plugins/ssr/ssrcommon.ml2
14 files changed, 43 insertions, 46 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index b9ad1ff6d8..07f50f6cd5 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -10,7 +10,7 @@
open Constr
-let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n)
+let bt_lib_constr n = lazy (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref n)
let decomp_term sigma (c : Constr.t) =
Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c)))
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 8fa676de44..b0c4785d7a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -233,12 +233,11 @@ let ll_forall_tac prod backtrack id continue seq=
(* special for compatibility with old Intuition *)
-let constant str = UnivGen.constr_of_global
- @@ Coqlib.lib_ref str
+let constant str = Coqlib.lib_ref str
let defined_connectives = lazy
- [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type")));
- AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))]
+ [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type"));
+ AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))]
let normalize_evaluables=
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 98d68d3db7..ad1114b733 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic =
let rec_pte_id = Id.of_string "Hrec"
let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
- let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in
- let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in
- let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in
+ let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in
+ let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in
+ let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in
let rec scan_type context type_of_hyp : tactic =
if isLetIn sigma type_of_hyp then
let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
@@ -1605,7 +1605,7 @@ let prove_principle_for_gen
match !tcc_lemma_ref with
| Undefined -> user_err Pp.(str "No tcc proof !!")
| Value lemma -> EConstr.of_constr lemma
- | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I")
+ | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I")
in
(* let rec list_diff del_list check_list = *)
(* match del_list with *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 03a64988e4..a385a61ae0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -116,7 +116,7 @@ let def_of_const t =
[@@@ocaml.warning "-3"]
let coq_constant s =
- UnivGen.constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition"
Coqlib.init_modules s;;
@@ -441,7 +441,7 @@ let jmeq () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
EConstr.of_constr @@
- UnivGen.constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.lib_ref "core.JMeq.type"
with e when CErrors.noncritical e -> raise (ToShow e)
@@ -449,7 +449,7 @@ let jmeq_refl () =
try
Coqlib.check_required_library Coqlib.jmeq_module_name;
EConstr.of_constr @@
- UnivGen.constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.lib_ref "core.JMeq.refl"
with e when CErrors.noncritical e -> raise (ToShow e)
@@ -463,7 +463,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
[@@@ocaml.warning "-3"]
-let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@
+let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof"
[@@@ocaml.warning "+3"]
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b8973a18dc..b0842c3721 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
let make_eq () =
try
- EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type"))
+ EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type"))
with _ -> assert false
(* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true]
@@ -511,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
intros_with_rewrite
] g
end
- | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) ->
+ | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) ->
Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENLIST[
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ca3160f4c4..f9df3aed45 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -51,7 +51,7 @@ open Context.Rel.Declaration
(* Ugly things which should not be here *)
[@@@ocaml.warning "-3"]
-let coq_constant m s = EConstr.of_constr @@ constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
Coqlib.find_reference "RecursiveDefinition" m s
let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
@@ -63,7 +63,7 @@ let pr_leconstr_rd =
let coq_init_constant s =
EConstr.of_constr (
- constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
[@@@ocaml.warning "+3"]
@@ -97,7 +97,7 @@ let type_of_const sigma t =
Typeops.type_of_constant_in (Global.env()) (sp, u)
|_ -> assert false
-let constant sl s = constr_of_global (find_reference sl s)
+let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s)
let const_of_ref = function
ConstRef kn -> kn
@@ -1241,7 +1241,7 @@ let get_current_subgoals_types () =
exception EmptySubgoals
let build_and_l sigma l =
- let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in
+ let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in
let conj_constr = Coqlib.build_coq_conj () in
let mk_and p1 p2 =
mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 1f2c722b34..a88285c9ee 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -115,7 +115,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
(* Summary and Object declaration *)
-open Nametab
open Libobject
type ltac_entry = {
@@ -153,19 +152,19 @@ let tac_deprecation kn =
let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
- let () = if not local then push_tactic (Until i) sp kn in
+ let () = if not local then push_tactic (Nametab.Until i) sp kn in
add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
- let () = if not local then push_tactic (Exactly i) sp kn in
+ let () = if not local then push_tactic (Nametab.Exactly i) sp kn in
add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with
| None ->
- let () = push_tactic (Until 1) sp kn in
+ let () = push_tactic (Nametab.Until 1) sp kn in
add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 5501cf92a5..55412c74bb 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -19,7 +19,6 @@ open Util
open Names
open Libnames
open Globnames
-open Nametab
open Smartlocate
open Constrexpr
open Termops
@@ -98,7 +97,7 @@ let intern_global_reference ist qid =
ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
else
try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
- with Not_found -> error_global_not_found qid
+ with Not_found -> Nametab.error_global_not_found qid
let intern_ltac_variable ist qid =
if qualid_is_ident qid && find_var (qualid_basename qid) ist then
@@ -150,7 +149,7 @@ let intern_isolated_tactic_reference strict ist qid =
try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
with Not_found ->
(* Reference not found *)
- error_global_not_found qid
+ Nametab.error_global_not_found qid
(* Internalize an applied tactic reference *)
@@ -169,7 +168,7 @@ let intern_applied_tactic_reference ist qid =
try intern_applied_global_tactic_reference qid
with Not_found ->
(* Reference not found *)
- error_global_not_found qid
+ Nametab.error_global_not_found qid
(* Intern a reference parsed in a non-tactic entry *)
@@ -190,7 +189,7 @@ let intern_non_tactic_reference strict ist qid =
TacGeneric ipat
else
(* Reference not found *)
- error_global_not_found qid
+ Nametab.error_global_not_found qid
let intern_message_token ist = function
| (MsgString _ | MsgInt _ as x) -> x
@@ -302,7 +301,7 @@ let intern_evaluable_global_reference ist qid =
try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
with Not_found ->
if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
- else error_global_not_found qid
+ else Nametab.error_global_not_found qid
let intern_evaluable_reference_or_by_notation ist = function
| {v=AN r} -> intern_evaluable_global_reference ist r
@@ -377,7 +376,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
subterm matched when a pattern *)
let r = match r with
| {v=AN r} -> r
- | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in
+ | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in
let sign = {
Constrintern.ltac_vars = ist.ltacvars;
ltac_bound = Id.Set.empty;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f90e889678..b60b77595b 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -23,7 +23,6 @@ open Names
open Nameops
open Libnames
open Globnames
-open Nametab
open Refiner
open Tacmach.New
open Tactic_debug
@@ -358,7 +357,7 @@ let interp_reference ist env sigma = function
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
- with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
+ with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
let try_interp_evaluable env (loc, id) =
let v = Environ.lookup_named id env in
@@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function
with Not_found ->
match r with
| EvalConstRef _ -> r
- | _ -> error_global_not_found (qualid_of_ident ?loc id)
+ | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
end
| ArgArg (r,None) -> r
| ArgVar {loc;v=id} ->
try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try try_interp_evaluable env (loc, id)
- with Not_found -> error_global_not_found (qualid_of_ident ?loc id)
+ with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
(try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
- error_global_not_found (qualid_of_ident ?loc id))
+ Nametab.error_global_not_found (qualid_of_ident ?loc id))
| Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (interp_typed_pattern ist env sigma c) in
interp_occurrences ist occs, p
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 11d0a4a44d..ef60a23e80 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -135,7 +135,7 @@ let mul = function
| (Const n,q) when eq_num n num_1 -> q
| (p,q) -> Mul(p,q)
-let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n))
+let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
let tpexpr = gen_constant "plugins.setoid_ring.pexpr"
let ttconst = gen_constant "plugins.setoid_ring.const"
@@ -540,7 +540,7 @@ let nsatz lpol =
let return_term t =
let a =
- mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in
+ mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in
let a = EConstr.of_constr a in
generalize [a]
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 09bd4cd352..d8adb17710 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -186,7 +186,8 @@ let reset_all () =
To use the constant Zplus, one must type "Lazy.force coq_Zplus"
This is the right way to access to Coq constants in tactics ML code *)
-let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr)
+let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global
+ |> EConstr.of_constr)
(* Zarith *)
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 79418da27c..840a05e02b 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -26,11 +26,11 @@ let step_count = ref 0
let node_count = ref 0
-let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type"))
-let li_and = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type"))
-let li_or = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type"))
+let li_False = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type"))
+let li_and = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type"))
+let li_or = lazy (destInd (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.or.type"))
-let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n))
+let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n))
let l_xI = gen_constant "num.pos.xI"
let l_xO = gen_constant "num.pos.xO"
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9585826109..8dbef47fe1 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -206,7 +206,7 @@ let exec_tactic env evd n f args =
let nf c = constr_of evd c in
Array.map nf !tactic_res, Evd.universe_context_set evd
-let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n)))
+let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)))
let gen_reference n = lazy (Coqlib.lib_ref n)
let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory"
@@ -251,7 +251,7 @@ let plugin_modules =
]
let my_constant c =
- lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
+ lazy (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
[@@ocaml.warning "-3"]
let my_reference c =
lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
@@ -901,7 +901,7 @@ let ftheory_to_obj : field_info -> obj =
let field_equality evd r inv req =
match EConstr.kind !evd req with
| App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
- let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in
+ let c = UnivGen.constr_of_monomorphic_global Coqlib.(lib_ref "core.eq.congr") in
let c = EConstr.of_constr c in
mkApp(c,[|r;r;inv|])
| _ ->
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1492cfb4e4..6746eff223 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1220,7 +1220,7 @@ let genclrtac cl cs clr =
(fun type_err gl ->
tclTHEN
(tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr
- (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr))
+ (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr))
(fun gl -> raise type_err)
gl))
(old_cleartac clr)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:45:38 +0000