aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml8
-rw-r--r--plugins/funind/functional_principles_types.ml14
-rw-r--r--plugins/funind/indfun_common.ml10
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/plugin_base.dune1
-rw-r--r--plugins/funind/recdef.ml12
6 files changed, 26 insertions, 23 deletions
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/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9ca91d62da..d57b931785 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -676,11 +676,15 @@ let build_case_scheme fa =
(* in *)
let funs =
let (_,f,_) = fa in
- try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
+ try (let open GlobRef in
+ match Smartlocate.global_with_alias f with
+ | ConstRef c -> c
+ | IndRef _ | ConstructRef _ | VarRef _ -> assert false)
with Not_found ->
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_qualid f) in
- let first_fun,u = destConst funs in
+ let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
+ let first_fun = funs in
let funs_mp = Constant.modpath first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
@@ -688,7 +692,7 @@ let build_case_scheme fa =
let prop_sort = InProp in
let funs_indexes =
let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
- List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
+ List.assoc_f Constant.equal funs this_block_funs_indexes
in
let (ind, sf) =
let ind = first_fun_kn,funs_indexes in
@@ -700,7 +704,7 @@ let build_case_scheme fa =
let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
let sorts =
(fun (_,_,x) ->
- UnivGen.new_sort_in_family x
+ fst @@ UnivGen.fresh_sort_in_family x
)
fa
in
@@ -718,7 +722,7 @@ let build_case_scheme fa =
(Some princ_name)
this_block_funs
0
- (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|])
+ (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|])
in
()
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 03a64988e4..28a9542167 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;;
@@ -311,7 +311,7 @@ let pr_info f_info =
str "function_constant_type := " ++
(try
Printer.pr_lconstr_env env sigma
- (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
+ (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
@@ -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/plugin_base.dune b/plugins/funind/plugin_base.dune
index 002eb28eea..9f583234d8 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -2,4 +2,5 @@
(name recdef_plugin)
(public_name coq.plugins.recdef)
(synopsis "Coq's functional induction plugin")
+ (flags :standard -open Gramlib)
(libraries coq.plugins.extraction))
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9fa333c629..f9df3aed45 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -24,6 +24,7 @@ open Globnames
open Nameops
open CErrors
open Util
+open UnivGen
open Tacticals
open Tacmach
open Tactics
@@ -50,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 @@ UnivGen.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"]
@@ -62,7 +63,7 @@ let pr_leconstr_rd =
let coq_init_constant s =
EConstr.of_constr (
- UnivGen.constr_of_global @@
+ UnivGen.constr_of_monomorphic_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
[@@@ocaml.warning "+3"]
@@ -96,10 +97,7 @@ let type_of_const sigma t =
Typeops.type_of_constant_in (Global.env()) (sp, u)
|_ -> assert false
-let constr_of_global x =
- fst (Global.constr_of_global_in_context (Global.env ()) x)
-
-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
@@ -1243,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 01:02:49 +0000