aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/FunInd.v12
-rw-r--r--plugins/funind/Recdef.v52
-rw-r--r--plugins/funind/functional_principles_proofs.ml58
-rw-r--r--plugins/funind/functional_principles_types.ml8
-rw-r--r--plugins/funind/functional_principles_types.mli4
-rw-r--r--plugins/funind/g_indfun.mlg4
-rw-r--r--plugins/funind/gen_principle.ml19
-rw-r--r--plugins/funind/gen_principle.mli4
-rw-r--r--plugins/funind/glob_term_to_relation.ml29
-rw-r--r--plugins/funind/glob_termops.ml4
-rw-r--r--plugins/funind/glob_termops.mli4
-rw-r--r--plugins/funind/indfun.ml25
-rw-r--r--plugins/funind/indfun.mli4
-rw-r--r--plugins/funind/indfun_common.ml34
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/invfun.ml10
-rw-r--r--plugins/funind/invfun.mli4
-rw-r--r--plugins/funind/recdef.ml82
18 files changed, 140 insertions, 219 deletions
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
deleted file mode 100644
index d58b169154..0000000000
--- a/plugins/funind/FunInd.v
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <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) *)
-(************************************************************************)
-
-Require Coq.extraction.Extraction.
-Declare ML Module "recdef_plugin".
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
deleted file mode 100644
index cd3d69861f..0000000000
--- a/plugins/funind/Recdef.v
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <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) *)
-(************************************************************************)
-
-Require Export Coq.funind.FunInd.
-Require Import PeanoNat.
-Require Compare_dec.
-Require Wf_nat.
-
-Section Iter.
-Variable A : Type.
-
-Fixpoint iter (n : nat) : (A -> A) -> A -> A :=
- fun (fl : A -> A) (def : A) =>
- match n with
- | O => def
- | S m => fl (iter m fl def)
- end.
-End Iter.
-
-Theorem le_lt_SS x y : x <= y -> x < S (S y).
-Proof.
- intros. now apply Nat.lt_succ_r, Nat.le_le_succ_r.
-Qed.
-
-Theorem Splus_lt x y : y < S (x + y).
-Proof.
- apply Nat.lt_succ_r. rewrite Nat.add_comm. apply Nat.le_add_r.
-Qed.
-
-Theorem SSplus_lt x y : x < S (S (x + y)).
-Proof.
- apply le_lt_SS, Nat.le_add_r.
-Qed.
-
-Inductive max_type (m n:nat) : Set :=
- cmt : forall v, m <= v -> n <= v -> max_type m n.
-
-Definition max m n : max_type m n.
-Proof.
- destruct (Compare_dec.le_gt_dec m n) as [h|h].
- - exists n; [exact h | apply le_n].
- - exists m; [apply le_n | apply Nat.lt_le_incl; exact h].
-Defined.
-
-Definition Acc_intro_generator_function := fun A R => @Acc_intro_generator A R 100.
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 6db0a1119b..9749af1e66 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -475,7 +475,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
tclIDTAC
in
try
- scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id]
+ scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id]
with TOREMOVE ->
thin [hyp_id],[]
@@ -525,7 +525,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps;
observe_tac "after_introduction" (fun g' ->
(* We get infos on the equations introduced*)
- let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
+ let new_term_value_eq = pf_get_hyp_typ g' heq_id in
(* compute the new value of the body *)
let new_term_value =
match EConstr.kind (project g') new_term_value_eq with
@@ -536,22 +536,23 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
);
anomaly (Pp.str "cannot compute new term value.")
in
- let fun_body =
- mkLambda(make_annot Anonymous Sorts.Relevant,
- pf_unsafe_type_of g' term,
- Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
- )
- in
- let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
- let new_infos =
- {dyn_infos with
+ let g', termtyp = tac_type_of g' term in
+ let fun_body =
+ mkLambda(make_annot Anonymous Sorts.Relevant,
+ termtyp,
+ Termops.replace_term (project g') term (mkRel 1) dyn_infos.info
+ )
+ in
+ let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
+ let new_infos =
+ {dyn_infos with
info = new_body;
eq_hyps = heq_id::dyn_infos.eq_hyps
- }
- in
- clean_goal_with_heq ptes_infos continue_tac new_infos g'
- )])
- ]
+ }
+ in
+ clean_goal_with_heq ptes_infos continue_tac new_infos g'
+ )])
+ ]
g
@@ -633,7 +634,7 @@ let build_proof
let dyn_infos = {dyn_info' with info =
mkCase(ci,ct,t,cb)} in
let g_nb_prod = nb_prod (project g) (pf_concl g) in
- let type_of_term = pf_unsafe_type_of g t in
+ let g, type_of_term = tac_type_of g t in
let term_eq =
make_refl_eq (Lazy.force refl_equal) type_of_term t
in
@@ -849,7 +850,7 @@ let generalize_non_dep hyp g =
(* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
let hyps = [hyp] in
let env = Global.env () in
- let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
+ let hyp_typ = pf_get_hyp_typ g hyp in
let to_revert,_ =
let open Context.Named.Declaration in
Environ.fold_named_context_reverse (fun (clear,keep) decl ->
@@ -1351,7 +1352,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
let rewrite =
tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
in
- let _,hrec_concl = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in
+ let _,hrec_concl = decompose_prod (project gls) (pf_get_hyp_typ gls hrec) in
let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in
let f = (fst (destApp (project gls) f_app)) in
let rec backtrack : tactic =
@@ -1573,19 +1574,16 @@ let prove_principle_for_gen
(List.rev_map (get_name %> Nameops.Name.get_id)
(princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
);
- (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
- (Name acc_rec_arg_id)
- (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
- (Proofview.V82.tactic prove_rec_arg_acc)
- );
-(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
-(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *)
-(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
- (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1)));
-(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
+ Proofview.V82.of_tactic
+ (assert_by
+ (Name acc_rec_arg_id)
+ (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+ (Proofview.V82.tactic prove_rec_arg_acc));
+ (revert (List.rev (acc_rec_arg_id::args_ids)));
+ (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1)));
h_intros (List.rev (acc_rec_arg_id::args_ids));
Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
- (* observe_tac "finish" *) (fun gl' ->
+ (fun gl' ->
let body =
let _,args = destApp (project gl') (pf_concl gl') in
Array.last args
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 797d421c56..163645b719 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -63,14 +63,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
(* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *)
let change_predicate_sort i decl =
let new_sort = sorts.(i) in
- let args,_ = decompose_prod (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in
+ let args,_ = decompose_prod_assum (EConstr.Unsafe.to_constr (RelDecl.get_type decl)) in
let real_args =
if princ_type_info.indarg_in_concl
then List.tl args
else args
in
Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl),
- Term.compose_prod real_args (mkSort new_sort))
+ Term.it_mkProd_or_LetIn (mkSort new_sort) real_args)
in
let new_predicates =
List.map_i
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 6f060b0146..c870603a43 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index a02cb24bee..68e1087b74 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 58efee1518..446026c4c8 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -295,8 +295,9 @@ let generate_functional_principle (evd: Evd.evar_map ref)
~name:new_princ_name ~hook_data
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
~kind:Decls.(IsProof Theorem)
- UnivNames.empty_binders
- entry [] in
+ ~ubind:UnivNames.empty_binders
+ ~impargs:[]
+ entry in
()
with e when CErrors.noncritical e ->
raise (Defining_principle e)
@@ -617,7 +618,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
let constructor_args g =
List.fold_right
(fun hid acc ->
- let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+ let type_of_hid = pf_get_hyp_typ g hid in
let sigma = project g in
match EConstr.kind sigma type_of_hid with
| Prod(_,_,t') ->
@@ -953,7 +954,7 @@ let rec reflexivity_with_destruct_cases g =
match sc with
None -> tclIDTAC g
| Some id ->
- match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with
+ match EConstr.kind (project g) (pf_get_hyp_typ g id) with
| App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -993,7 +994,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
(* We get the constant and the principle corresponding to this lemma *)
let f = funcs.(i) in
let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i)) in
- let princ_type = pf_unsafe_type_of g graph_principle in
+ let g, princ_type = tac_type_of g graph_principle in
let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
(* Then we get the number of argument of the function
and compute a fresh name for each of them
@@ -1210,7 +1211,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
in
let _ = evd := sigma in
let l_schemes =
- List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
+ List.map (EConstr.of_constr %> Retyping.get_type_of env sigma %> EConstr.Unsafe.to_constr) schemes
in
let i = ref (-1) in
let sorts =
@@ -2051,7 +2052,7 @@ let build_case_scheme fa =
let (sigma, scheme) =
Indrec.build_case_analysis_scheme_default env sigma ind sf
in
- let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
+ let scheme_type = EConstr.Unsafe.to_constr ((Retyping.get_type_of env sigma) (EConstr.of_constr scheme)) in
let sorts =
(fun (_,_,x) ->
fst @@ UnivGen.fresh_sort_in_family x
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli
index 7eb8ca3af1..6313a2b16e 100644
--- a/plugins/funind/gen_principle.mli
+++ b/plugins/funind/gen_principle.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e41b92d4dc..e08ad9af3a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -514,8 +514,9 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
a pseudo value "v1 ... vn".
The "value" of this branch is then simply [res]
*)
+ (* XXX here and other [understand] calls drop the ctx *)
let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
- let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in
+ let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in
let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
let res = fresh_id args_res.to_avoid "_res" in
let new_avoid = res::args_res.to_avoid in
@@ -629,7 +630,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
let v_res = build_entry_lc env sigma funnames avoid v in
let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
- let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in
+ let v_type = Retyping.get_type_of env (Evd.from_env env) v_as_constr in
let v_r = Sorts.Relevant in (* TODO relevance *)
let new_env =
match n with
@@ -646,7 +647,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
build_entry_lc_from_case env sigma funnames make_discr el brl avoid
| GIf(b,(na,e_option),lhs,rhs) ->
let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
- let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+ let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
@@ -678,7 +679,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
nal
in
let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
- let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
+ let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
let (ind,_) =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
@@ -723,7 +724,7 @@ and build_entry_lc_from_case env sigma funname make_discr
let types =
List.map (fun (case_arg,_) ->
let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in
- EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr)
+ EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr)
) el
in
(****** The next works only if the match is not dependent ****)
@@ -769,9 +770,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to
let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
List.fold_right
(fun id acc ->
- let typ_of_id =
- Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
- in
+ let typ_of_id = Typing.type_of_variable env_with_pat_ids id in
let raw_typ_of_id =
Detyping.detype Detyping.Now false Id.Set.empty
env_with_pat_ids (Evd.from_env env) typ_of_id
@@ -832,7 +831,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to
(fun id acc ->
if Id.Set.mem id this_pat_ids
then (Prod (Name id),
- let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
+ let typ_of_id = Typing.type_of_variable new_env id in
let raw_typ_of_id =
Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
in
@@ -1166,7 +1165,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let evd = (Evd.from_env env) in
let t',ctx = Pretyping.understand env evd t in
let evd = Evd.from_ctx ctx in
- let type_t' = Typing.unsafe_type_of env evd t' in
+ let type_t' = Retyping.get_type_of env evd t' in
let t' = EConstr.Unsafe.to_constr t' in
let type_t' = EConstr.Unsafe.to_constr type_t' in
let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in
@@ -1477,7 +1476,7 @@ let do_build_inductive
in
let rel_ind i ext_rel_constructors =
((CAst.make @@ relnames.(i)),
- rel_params,
+ (rel_params,None),
Some rel_arities.(i),
ext_rel_constructors),[]
in
@@ -1513,12 +1512,12 @@ let do_build_inductive
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
let repacked_rel_inds =
- List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+ List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn )
rel_inds
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
+ Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
++ fnl () ++
msg
in
@@ -1528,12 +1527,12 @@ let do_build_inductive
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
let repacked_rel_inds =
- List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+ List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn )
rel_inds
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
+ Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index f2d98a13ab..9fa72919ce 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index bdde66bbd7..c55fdc017c 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a205c0744a..1f2f56ec34 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -64,12 +64,10 @@ let functional_induction with_clean c princl pat =
| InSet -> finfo.rec_lemma
| InType -> finfo.rect_lemma
in
- let princ = (* then we get the principle *)
+ let sigma, princ = (* then we get the principle *)
match princ_option with
| Some princ ->
- let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in
- Proofview.Unsafe.tclEVARS sigma >>= fun () ->
- Proofview.tclUNIT princ
+ Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ)
| None ->
(*i If there is not default lemma defined then,
we cross our finger and try to find a lemma named f_ind
@@ -87,19 +85,18 @@ let functional_induction with_clean c princl pat =
user_err (str "Cannot find induction principle for "
++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
in
- let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in
- Proofview.Unsafe.tclEVARS sigma >>= fun () ->
- Proofview.tclUNIT princ
+ Evd.fresh_global (pf_env gl) (project gl) princ_ref
in
- princ >>= fun princ ->
- (* We need to refresh gl due to the updated evar_map in princ *)
- Proofview.Goal.enter_one (fun gl ->
- Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args))
+ let princt = Retyping.get_type_of (pf_env gl) sigma princ in
+ Proofview.Unsafe.tclEVARS sigma <*>
+ Proofview.tclUNIT (princ, Tactypes.NoBindings, princt, args)
| _ ->
CErrors.user_err (str "functional induction must be used with a function" )
end
| Some ((princ,binding)) ->
- Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args)
+ let sigma, princt = pf_type_of gl princ in
+ Proofview.Unsafe.tclEVARS sigma <*>
+ Proofview.tclUNIT (princ, binding, princt, args)
) >>= fun (princ, bindings, princ_type, args) ->
Proofview.Goal.enter (fun gl ->
let sigma = project gl in
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 476d74b3f8..4f3d4a1587 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b55d8537d6..7d87fc0220 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -92,18 +92,14 @@ let list_union_eq eq_fun l1 l2 =
let list_add_set_eq eq_fun x l =
if List.exists (eq_fun x) l then l else x::l
-[@@@ocaml.warning "-3"]
-let coq_constant s =
- UnivGen.constr_of_monomorphic_global @@
- Coqlib.gen_reference_in_modules "RecursiveDefinition"
- Coqlib.init_modules s;;
+let coq_constant s = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s;;
let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
Nametab.locate (make_qualid dp (Id.of_string s))
-let eq = lazy(EConstr.of_constr (coq_constant "eq"))
-let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
+let eq = lazy(EConstr.of_constr (coq_constant "core.eq.type"))
+let refl_equal = lazy(EConstr.of_constr (coq_constant "core.eq.refl"))
let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
@@ -320,7 +316,6 @@ open Goptions
let functional_induction_rewrite_dependent_proofs_sig =
{
optdepr = false;
- optname = "Functional Induction Rewrite Dependent";
optkey = ["Functional";"Induction";"Rewrite";"Dependent"];
optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b)
@@ -332,7 +327,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t
let function_debug_sig =
{
optdepr = false;
- optname = "Function debug";
optkey = ["Function_debug"];
optread = (fun () -> !function_debug);
optwrite = (fun b -> function_debug := b)
@@ -371,10 +365,10 @@ let do_observe_tac s tac g =
ignore(Stack.pop debug_queue);
v
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
if not (Stack.is_empty debug_queue)
then print_debug_queue true (fst reraise);
- Util.iraise reraise
+ Exninfo.iraise reraise
let observe_tac s tac g =
if do_observe ()
@@ -416,7 +410,6 @@ let is_strict_tcc () = !strict_tcc
let strict_tcc_sig =
{
optdepr = false;
- optname = "Raw Function Tcc";
optkey = ["Function_raw_tcc"];
optread = (fun () -> !strict_tcc);
optwrite = (fun b -> strict_tcc := b)
@@ -450,14 +443,11 @@ let h_intros l =
let h_id = Id.of_string "h"
let hrec_id = Id.of_string "hrec"
-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")
+let well_founded = function () -> EConstr.of_constr (coq_constant "core.wf.well_founded")
+let acc_rel = function () -> EConstr.of_constr (coq_constant "core.wf.acc")
+let acc_inv_id = function () -> EConstr.of_constr (coq_constant "core.wf.acc_inv")
-[@@@ocaml.warning "-3"]
-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"]
+let well_founded_ltof () = EConstr.of_constr (coq_constant "num.nat.well_founded_ltof")
let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
@@ -523,6 +513,10 @@ let funind_purify f x =
let st = Vernacstate.freeze_interp_state ~marshallable:false in
try f x
with e ->
- let e = CErrors.push e in
+ let e = Exninfo.capture e in
Vernacstate.unfreeze_interp_state st;
Exninfo.iraise e
+
+let tac_type_of g c =
+ let sigma, t = Tacmach.pf_type_of g c in
+ {g with Evd.sigma}, t
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 550f727951..bd8b34088b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -119,3 +119,5 @@ type tcc_lemma_value =
| Not_needed
val funind_purify : ('a -> 'b) -> ('a -> 'b)
+
+val tac_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Goal.goal Evd.sigma * EConstr.types
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d72319d078..44d2cb4a3d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -28,7 +28,7 @@ open Indfun_common
*)
let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
let sigma = project gl in
- let typ = pf_unsafe_type_of gl (mkVar hid) in
+ let typ = pf_get_hyp_typ hid gl in
match EConstr.kind sigma typ with
| App(i,args) when isInd sigma i ->
let ((kn',num) as ind'),u = destInd sigma i in
@@ -77,7 +77,7 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl ->
let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in
let sigma = project gl in
- let type_of_h = pf_unsafe_type_of gl (mkVar hid) in
+ let type_of_h = pf_get_hyp_typ hid gl in
match EConstr.kind sigma type_of_h with
| App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
let pre_tac,f_args,res =
@@ -128,7 +128,7 @@ let invfun qhyp f =
| None ->
let tac_action hid gl =
let sigma = project gl in
- let hyp_typ = pf_unsafe_type_of gl (mkVar hid) in
+ let hyp_typ = pf_get_hyp_typ hid gl in
match EConstr.kind sigma hyp_typ with
| App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
begin
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 6b789e1bb2..41dbe1437c 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 66ed1961ba..19a762d33d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -31,7 +31,6 @@ open Tactics
open Nametab
open Declare
open Tacred
-open Goal
open Glob_term
open Pretyping
open Termops
@@ -48,18 +47,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_monomorphic_global @@
- Coqlib.find_reference "RecursiveDefinition" m s
-
-let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
-let arith_Lt = ["Coq"; "Arith";"Lt"]
+let coq_constant s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
+ Coqlib.lib_ref s
let coq_init_constant s =
- EConstr.of_constr (
- UnivGen.constr_of_monomorphic_global @@
- Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
-[@@@ocaml.warning "+3"]
+ EConstr.of_constr(UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s)
+;;
let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
@@ -110,9 +103,10 @@ let pf_get_new_ids idl g =
let next_ident_away_in_goal ids avoid =
next_ident_away_in_goal ids (Id.Set.of_list avoid)
-let compute_renamed_type gls c =
+let compute_renamed_type gls id =
rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) []
- (pf_unsafe_type_of gls c)
+ (pf_get_hyp_typ gls id)
+
let h'_id = Id.of_string "h'"
let teq_id = Id.of_string "teq"
let ano_id = Id.of_string "anonymous"
@@ -122,26 +116,26 @@ let v_id = Id.of_string "v"
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")
+let lt = function () -> (coq_init_constant "num.nat.lt")
+let le = function () -> Coqlib.lib_ref "num.nat.le"
+
+let ex = function () -> (coq_init_constant "core.ex.type")
+let nat = function () -> (coq_init_constant "num.nat.type")
let iter_ref () =
try find_reference ["Recdef"] "iter"
with Not_found -> user_err Pp.(str "module Recdef not loaded")
let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref))
-let eq = function () -> (coq_init_constant "eq")
+let eq = function () -> (coq_init_constant "core.eq.type")
let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
-let le_trans = function () -> (coq_constant arith_Nat "le_trans")
-let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans")
-let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n")
-let le_n = function () -> (coq_init_constant "le_n")
+let le_lt_n_Sm = function () -> (coq_constant "num.nat.le_lt_n_Sm")
+let le_trans = function () -> (coq_constant "num.nat.le_trans")
+let le_lt_trans = function () -> (coq_constant "num.nat.le_lt_trans")
+let lt_S_n = function () -> (coq_constant "num.nat.lt_S_n")
+let le_n = function () -> (coq_init_constant "num.nat.le_n")
let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
-let coq_O = function () -> (coq_init_constant "O")
-let coq_S = function () -> (coq_init_constant "S")
-let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
+let coq_O = function () -> (coq_init_constant "num.nat.O")
+let coq_S = function () -> (coq_init_constant"num.nat.S")
+let lt_n_O = function () -> (coq_constant "num.nat.nlt_0_r")
let max_ref = function () -> (find_reference ["Recdef"] "max")
let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref))
@@ -370,7 +364,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
Proofview.V82.of_tactic (clear to_intros);
h_intros to_intros;
(fun g' ->
- let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
+ let ty_teq = pf_get_hyp_typ g' heq in
let teq_lhs,teq_rhs =
let _,args = try destApp (project g') ty_teq with DestKO -> assert false in
args.(1),args.(2)
@@ -487,13 +481,13 @@ let rec prove_lt hyple g =
in
let h =
List.find (fun id ->
- match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with
+ match decompose_app sigma (pf_get_hyp_typ g id) with
| _, t::_ -> EConstr.eq_constr sigma t varx
| _ -> false
) hyple
in
let y =
- List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in
+ List.hd (List.tl (snd (decompose_app sigma (pf_get_hyp_typ g h)))) in
observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[
Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple)
@@ -645,9 +639,7 @@ let pf_typel l tac =
modified hypotheses are generalized in the process and should be
introduced back later; the result is the pair of the tactic and the
list of hypotheses that have been generalized and cleared. *)
-let mkDestructEq :
- Id.t list -> constr -> goal Evd.sigma -> tactic * Id.t list =
- fun not_on_hyp expr g ->
+let mkDestructEq not_on_hyp expr g =
let hyps = pf_hyps g in
let to_revert =
Util.List.map_filter
@@ -657,9 +649,9 @@ let mkDestructEq :
if Id.List.mem id not_on_hyp || not (Termops.dependent (project g) expr (get_type decl))
then None else Some id) hyps in
let to_revert_constr = List.rev_map mkVar to_revert in
- let type_of_expr = pf_unsafe_type_of g expr in
- let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
- to_revert_constr in
+ let g, type_of_expr = tac_type_of g expr in
+ let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::to_revert_constr in
+ let tac =
pf_typel new_hyps (fun _ ->
observe_tclTHENLIST (fun _ _ -> str "mkDestructEq")
[Proofview.V82.of_tactic (generalize new_hyps);
@@ -668,7 +660,9 @@ let mkDestructEq :
pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
in
Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2);
- Proofview.V82.of_tactic (simplest_case expr)]), to_revert
+ Proofview.V82.of_tactic (simplest_case expr)])
+ in
+ g, tac, to_revert
let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
let sigma = project g in
@@ -686,7 +680,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
info = mkCase(ci,t,a',l);
is_main_branch = expr_info.is_main_branch;
is_final = expr_info.is_final} in
- let destruct_tac,rev_to_thin_intro =
+ let g,destruct_tac,rev_to_thin_intro =
mkDestructEq [expr_info.rec_arg_id] a' g in
let to_thin_intro = List.rev rev_to_thin_intro in
observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
@@ -817,7 +811,7 @@ let rec prove_le g =
| App (c, [| x0 ; _ |]) ->
EConstr.isVar sigma x0 &&
Id.equal (destVar sigma x0) (destVar sigma x) &&
- EConstr.is_global sigma (le ()) c
+ EConstr.isRefX sigma (le ()) c
| _ -> false
in
let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in
@@ -842,7 +836,7 @@ let rec make_rewrite_list expr_info max = function
(observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) (
(fun g ->
let sigma = project g in
- let t_eq = compute_renamed_type g (mkVar hp) in
+ let t_eq = compute_renamed_type g hp in
let k,def =
let k_na,_,t = destProd sigma t_eq in
let _,_,t = destProd sigma t in
@@ -868,7 +862,7 @@ let make_rewrite expr_info l hp max =
(observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS
(fun g ->
let sigma = project g in
- let t_eq = compute_renamed_type g (mkVar hp) in
+ let t_eq = compute_renamed_type g hp in
let k,def =
let k_na,_,t = destProd sigma t_eq in
let _,_,t = destProd sigma t in
@@ -1194,7 +1188,7 @@ let get_current_subgoals_types pstate =
exception EmptySubgoals
let build_and_l sigma l =
let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in
- let conj_constr = Coqlib.build_coq_conj () in
+ let conj_constr = Coqlib.lib_ref "core.and.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-02 00:09:05 +0000