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.ml30
-rw-r--r--plugins/funind/glob_term_to_relation.ml13
-rw-r--r--plugins/funind/glob_termops.ml4
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/indfun_common.ml40
-rw-r--r--plugins/funind/invfun.ml9
-rw-r--r--plugins/funind/recdef.ml16
8 files changed, 54 insertions, 70 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5336948642..b12364d04a 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.build_coq_False ()) in
- let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in
- let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in
+ 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 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.build_coq_I ())
+ | Not_needed -> EConstr.of_constr (UnivGen.constr_of_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 b2a528a1fd..9ca91d62da 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
open Printer
open CErrors
open Term
@@ -322,7 +332,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
try
let f = funs.(i) in
- let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in
+ let sigma, type_sort = Evd.fresh_sort_in_family !evd InType in
+ evd := sigma;
let new_sorts =
match sorts with
| None -> Array.make (Array.length funs) (type_sort)
@@ -394,7 +405,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
exception Not_Rec
-let get_funs_constant mp dp =
+let get_funs_constant mp =
let get_funs_constant const e : (Names.Constant.t*int) array =
match Constr.kind ((strip_lam e)) with
| Fix((_,(na,_,_))) ->
@@ -402,7 +413,7 @@ let get_funs_constant mp dp =
(fun i na ->
match na with
| Name id ->
- let const = Constant.make3 mp dp (Label.of_id id) in
+ let const = Constant.make2 mp (Label.of_id id) in
const,i
| Anonymous ->
anomaly (Pp.str "Anonymous fix.")
@@ -474,13 +485,13 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
- let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in
+ let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
let first_fun_kn =
try
fst (find_Function_infos (fst first_fun)).graph_ind
with Not_found -> raise No_graph_found
in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in
+ let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
@@ -507,8 +518,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let i = ref (-1) in
let sorts =
List.rev_map (fun (_,x) ->
- Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x
- )
+ let sigma, fs = Evd.fresh_sort_in_family !evd x in
+ evd := sigma; fs
+ )
fas
in
(* We create the first priciple by tactic *)
@@ -669,9 +681,9 @@ let build_case_scheme fa =
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_qualid f) in
let first_fun,u = destConst funs in
- let funs_mp,funs_dp,_ = Constant.repr3 first_fun 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 funs_dp first_fun in
+ let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0c45de4dc4..7c80b776a4 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -259,11 +259,8 @@ let mk_result ctxt value avoid =
Some functions to deal with overlapping patterns
**************************************************)
-let coq_True_ref =
- lazy (Coqlib.coq_reference "" ["Init";"Logic"] "True")
-
-let coq_False_ref =
- lazy (Coqlib.coq_reference "" ["Init";"Logic"] "False")
+let coq_True_ref = lazy (Coqlib.lib_ref "core.True.type")
+let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type")
(*
[make_discr_match_el \[e1,...en\]] builds match e1,...,en with
@@ -957,7 +954,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
assert false
end
| GApp(eq_as_ref,[ty; id ;rt])
- when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
+ when is_gvar id && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous
->
let loc1 = rt.CAst.loc in
let loc2 = eq_as_ref.CAst.loc in
@@ -1078,7 +1075,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
else new_b, Id.Set.add id id_to_exclude
*)
| GApp(eq_as_ref,[ty;rt1;rt2])
- when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
+ when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous
->
begin
try
@@ -1089,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
List.fold_left
(fun acc (lhs,rhs) ->
mkGProd(Anonymous,
- mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc)
+ mkGApp(mkGRef Coqlib.(lib_ref "core.eq.type"),[mkGHole ();lhs;rhs]),acc)
)
b
l
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index f81de82d5e..5b45a8dbed 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -38,11 +38,11 @@ let glob_decompose_app =
(* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *)
let glob_make_eq ?(typ= mkGHole ()) t1 t2 =
- mkGApp(mkGRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
+ mkGApp(mkGRef (Coqlib.lib_ref "core.eq.type"),[typ;t2;t1])
(* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *)
let glob_make_neq t1 t2 =
- mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2])
+ mkGApp(mkGRef (Coqlib.lib_ref "core.not.type"),[glob_make_eq t1 t2])
let remove_name_from_mapping mapping na =
match na with
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9eda19a86b..9a6169d42a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -898,11 +898,11 @@ let make_graph (f_ref : GlobRef.t) =
let id = Label.to_id (Constant.label c) in
[((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
- let mp,dp,_ = Constant.repr3 c in
+ let mp = Constant.modpath c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+ (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 4eee2c7a45..03a64988e4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -114,6 +114,7 @@ let def_of_const t =
with Not_found -> assert false)
|_ -> assert false
+[@@@ocaml.warning "-3"]
let coq_constant s =
UnivGen.constr_of_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition"
@@ -297,36 +298,7 @@ let subst_Function (subst,finfos) =
let classify_Function infos = Libobject.Substitute infos
-let discharge_Function (_,finfos) =
- let function_constant' = Lib.discharge_con finfos.function_constant
- and graph_ind' = Lib.discharge_inductive finfos.graph_ind
- and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
- and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
- and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
- and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
- and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
- and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
- in
- if function_constant' == finfos.function_constant &&
- graph_ind' == finfos.graph_ind &&
- equation_lemma' == finfos.equation_lemma &&
- correctness_lemma' == finfos.correctness_lemma &&
- completeness_lemma' == finfos.completeness_lemma &&
- rect_lemma' == finfos.rect_lemma &&
- rec_lemma' == finfos.rec_lemma &&
- prop_lemma' == finfos.prop_lemma
- then Some finfos
- else
- Some { function_constant = function_constant' ;
- graph_ind = graph_ind' ;
- equation_lemma = equation_lemma' ;
- correctness_lemma = correctness_lemma' ;
- completeness_lemma = completeness_lemma';
- rect_lemma = rect_lemma';
- rec_lemma = rec_lemma';
- prop_lemma = prop_lemma' ;
- is_general = finfos.is_general
- }
+let discharge_Function (_,finfos) = Some finfos
let pr_ocst c =
let sigma, env = Pfedit.get_current_context () in
@@ -470,7 +442,7 @@ let jmeq () =
Coqlib.check_required_library Coqlib.jmeq_module_name;
EConstr.of_constr @@
UnivGen.constr_of_global @@
- Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq"
+ Coqlib.lib_ref "core.JMeq.type"
with e when CErrors.noncritical e -> raise (ToShow e)
let jmeq_refl () =
@@ -478,7 +450,7 @@ let jmeq_refl () =
Coqlib.check_required_library Coqlib.jmeq_module_name;
EConstr.of_constr @@
UnivGen.constr_of_global @@
- Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl"
+ Coqlib.lib_ref "core.JMeq.refl"
with e when CErrors.noncritical e -> raise (ToShow e)
let h_intros l =
@@ -490,8 +462,10 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded"
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 @@
- Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof"
+ Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof"
+[@@@ocaml.warning "+3"]
let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ad11f853ca..b8973a18dc 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -81,10 +81,9 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
let make_eq () =
try
- EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ()))
- with _ -> assert false
+ EConstr.of_constr (UnivGen.constr_of_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]
(resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block.
@@ -450,7 +449,7 @@ let generalize_dependent_of x hyp g =
let tauto =
let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
let mp = ModPath.MPfile (DirPath.make dp) in
- let kn = KerName.make2 mp (Label.make "tauto") in
+ let kn = KerName.make mp (Label.make "tauto") in
Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
let body = Tacenv.interp_ltac kn in
Tacinterp.eval_tactic body
@@ -512,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.build_coq_False ())) ->
+ | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_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 7298342e1e..89dfb58017 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -49,11 +49,12 @@ 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 @@
- Coqlib.coq_reference "RecursiveDefinition" m s
+ Coqlib.find_reference "RecursiveDefinition" m s
-let arith_Nat = ["Arith";"PeanoNat";"Nat"]
-let arith_Lt = ["Arith";"Lt"]
+let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
+let arith_Lt = ["Coq"; "Arith";"Lt"]
let pr_leconstr_rd =
let sigma, env = Pfedit.get_current_context () in
@@ -63,6 +64,7 @@ let coq_init_constant s =
EConstr.of_constr (
UnivGen.constr_of_global @@
Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
+[@@@ocaml.warning "+3"]
let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -143,6 +145,7 @@ let def_id = Id.of_string "def"
let p_id = Id.of_string "p"
let rec_res_id = Id.of_string "rec_res";;
let lt = function () -> (coq_init_constant "lt")
+[@@@ocaml.warning "-3"]
let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le")
let ex = function () -> (coq_init_constant "ex")
let nat = function () -> (coq_init_constant "nat")
@@ -163,7 +166,6 @@ let coq_S = function () -> (coq_init_constant "S")
let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
let max_ref = function () -> (find_reference ["Recdef"] "max")
let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref))
-let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj"
let f_S t = mkApp(delayed_force coq_S, [|t|]);;
@@ -713,7 +715,7 @@ let mkDestructEq :
observe_tclTHENLIST (str "mkDestructEq")
[Proofview.V82.of_tactic (generalize new_hyps);
(fun g2 ->
- let changefun patvars sigma =
+ let changefun patvars env sigma =
pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
in
Proofview.V82.of_tactic (change_in_concl None changefun) g2);
@@ -1241,8 +1243,8 @@ let get_current_subgoals_types () =
exception EmptySubgoals
let build_and_l sigma l =
- let and_constr = UnivGen.constr_of_global @@ Coqlib.build_coq_and () in
- let conj_constr = coq_conj () in
+ let and_constr = UnivGen.constr_of_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
let rec is_well_founded t =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 01:33:06 +0000