aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/FunInd.v10
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/functional_principles_proofs.ml36
-rw-r--r--plugins/funind/functional_principles_proofs.mli6
-rw-r--r--plugins/funind/functional_principles_types.ml10
-rw-r--r--plugins/funind/functional_principles_types.mli6
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun.ml14
-rw-r--r--plugins/funind/indfun.mli2
-rw-r--r--plugins/funind/indfun_common.ml20
-rw-r--r--plugins/funind/indfun_common.mli22
-rw-r--r--plugins/funind/invfun.ml52
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/recdef.ml24
15 files changed, 112 insertions, 102 deletions
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
new file mode 100644
index 000000000..e40aea776
--- /dev/null
+++ b/plugins/funind/FunInd.v
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Coq.extraction.Extraction.
+Declare ML Module "recdef_plugin".
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index e4433247b..64f43b833 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -6,8 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+Require Export Coq.funind.FunInd.
Require Import PeanoNat.
-
Require Compare_dec.
Require Wf_nat.
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 023cbad43..ef894b239 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -106,7 +106,7 @@ let make_refl_eq constructor type_of_t t =
type pte_info =
{
- proving_tac : (Id.t list -> Tacmach.tactic);
+ proving_tac : (Id.t list -> Proof_type.tactic);
is_valid : constr -> bool
}
@@ -688,7 +688,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
let build_proof
(interactive_proof:bool)
- (fnames:constant list)
+ (fnames:Constant.t list)
ptes_infos
dyn_infos
: tactic =
@@ -708,13 +708,13 @@ let build_proof
let term_eq =
make_refl_eq (Lazy.force refl_equal) type_of_term t
in
- tclTHENSEQ
+ tclTHENLIST
[
Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
thin dyn_infos.rec_hyps;
Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
(fun g -> observe_tac "toto" (
- tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
+ tclTHENLIST [Proofview.V82.of_tactic (Simple.case t);
(fun g' ->
let g'_nb_prod = nb_prod (project g') (pf_concl g') in
let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -982,14 +982,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
(* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *)
- let f_id = Label.to_id (con_label (fst (destConst evd f))) in
+ let f_id = Label.to_id (Constant.label (fst (destConst evd f))) in
let prove_replacement =
- tclTHENSEQ
+ tclTHENLIST
[
tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro);
observe_tac "" (fun g ->
let rec_id = pf_nth_hyp_id g 1 in
- tclTHENSEQ
+ tclTHENLIST
[observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
(Proofview.V82.of_tactic intros_reflexivity)] g
@@ -1019,7 +1019,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in
mkConst (Option.get finfos.equation_lemma)
with (Not_found | Option.IsNone as e) ->
- let f_id = Label.to_id (con_label (fst (destConst !evd f))) in
+ let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
(*i The next call to mk_equation_id is valid since we will construct the lemma
Ensures by: obvious
i*)
@@ -1242,7 +1242,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
other_fix_infos 0)
in
let first_tac : tactic = (* every operations until fix creations *)
- tclTHENSEQ
+ tclTHENLIST
[ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params)));
observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates)));
observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches)));
@@ -1260,7 +1260,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let fix_info = Id.Map.find pte ptes_to_fix in
let nb_args = fix_info.nb_realargs in
- tclTHENSEQ
+ tclTHENLIST
[
(* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro));
(fun g -> (* replacement of the function by its body *)
@@ -1279,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
eq_hyps = []
}
in
- tclTHENSEQ
+ tclTHENLIST
[
observe_tac "do_replace"
(do_replace evd
@@ -1322,7 +1322,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
] gl
with Not_found ->
let nb_args = min (princ_info.nargs) (List.length ctxt) in
- tclTHENSEQ
+ tclTHENLIST
[
tclDO nb_args (Proofview.V82.of_tactic intro);
(fun g -> (* replacement of the function by its body *)
@@ -1343,7 +1343,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
}
in
let fname = destConst (project g) (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) in
- tclTHENSEQ
+ tclTHENLIST
[Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]);
let do_prove =
build_proof
@@ -1402,7 +1402,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
fun gls ->
(* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
(* let ids = hid::pf_ids_of_hyps gls in *)
- tclTHENSEQ
+ tclTHENLIST
[
(* generalize [lemma]; *)
(* h_intro hid; *)
@@ -1457,13 +1457,13 @@ let rec rewrite_eqs_in_eqs eqs =
let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
fun gls ->
- (tclTHENSEQ
+ (tclTHENLIST
[
backtrack_eqs_until_hrec hrec eqs;
(* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
(tclTHENS (* We must have exactly ONE subgoal !*)
(Proofview.V82.of_tactic (apply (mkVar hrec)))
- [ tclTHENSEQ
+ [ tclTHENLIST
[
(Proofview.V82.of_tactic (keep (tcc_hyps@eqs)));
(Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
@@ -1617,7 +1617,7 @@ let prove_principle_for_gen
(Id.of_string "prov")
hyps
in
- tclTHENSEQ
+ tclTHENLIST
[
Proofview.V82.of_tactic (generalize [lemma]);
Proofview.V82.of_tactic (Simple.intro hid);
@@ -1636,7 +1636,7 @@ let prove_principle_for_gen
]
gls
in
- tclTHENSEQ
+ tclTHENLIST
[
observe_tac "start_tac" start_tac;
h_intros
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 069f767dd..5bb288678 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -4,17 +4,17 @@ open Names
val prove_princ_for_struct :
Evd.evar_map ref ->
bool ->
- int -> constant array -> EConstr.constr array -> int -> Tacmach.tactic
+ int -> Constant.t array -> EConstr.constr array -> int -> Proof_type.tactic
val prove_principle_for_gen :
- constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
+ Constant.t * Constant.t * Constant.t -> (* name of the function, the functional and the fixpoint equation *)
Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *)
bool -> (* is that function uses measure *)
int -> (* the number of recursive argument *)
EConstr.types -> (* the type of the recursive argument *)
EConstr.constr -> (* the wf relation used to prove the function *)
- Tacmach.tactic
+ Proof_type.tactic
(* val is_pte : rel_declaration -> bool *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index fd4b52b65..70245a8b1 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -150,7 +150,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
([],[])
in
let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
- applist(new_f, new_args),
+ applistc new_f new_args,
list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
| LetIn(x,v,t,b) ->
compute_new_princ_type_for_letin remove env x v t b
@@ -330,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
match new_princ_name with
| Some (id) -> id,id
| None ->
- let id_of_f = Label.to_id (con_label (fst f)) in
+ let id_of_f = Label.to_id (Constant.label (fst f)) in
id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
in
let names = ref [new_princ_name] in
@@ -389,14 +389,14 @@ let generate_functional_principle (evd: Evd.evar_map ref)
exception Not_Rec
let get_funs_constant mp dp =
- let get_funs_constant const e : (Names.constant*int) array =
+ let get_funs_constant const e : (Names.Constant.t*int) array =
match kind_of_term ((strip_lam e)) with
| Fix((_,(na,_,_))) ->
Array.mapi
(fun i na ->
match na with
| Name id ->
- let const = make_con mp dp (Label.of_id id) in
+ let const = Constant.make3 mp dp (Label.of_id id) in
const,i
| Anonymous ->
anomaly (Pp.str "Anonymous fix.")
@@ -656,7 +656,7 @@ let build_case_scheme fa =
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_reference f) in
let first_fun,u = destConst funs in
- let funs_mp,funs_dp,_ = Names.repr_con first_fun in
+ let funs_mp,funs_dp,_ = Constant.repr3 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 = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index bf1906bfb..bb2b2d918 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -18,7 +18,7 @@ val generate_functional_principle :
(* induction principle on rel *)
types ->
(* *)
- sorts array option ->
+ Sorts.t array option ->
(* Name of the new principle *)
(Id.t) option ->
(* the compute functions to use *)
@@ -28,10 +28,10 @@ val generate_functional_principle :
(* The tactic to use to make the proof w.r
the number of params
*)
- (EConstr.constr array -> int -> Tacmach.tactic) ->
+ (EConstr.constr array -> int -> Proof_type.tactic) ->
unit
-val compute_new_princ_type_from_rel : constr array -> sorts array ->
+val compute_new_princ_type_from_rel : constr array -> Sorts.t array ->
types -> types
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d9cd026d8..1258c9286 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function
END
let pr_fun_scheme_arg (princ_name,fun_name,s) =
- Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
+ Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
Ppconstr.pr_glob_sort s
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index eae72d9e8..726a8203d 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -579,8 +579,8 @@ let ids_of_pat =
ids_of_pat Id.Set.empty
let id_of_name = function
- | Names.Anonymous -> Id.of_string "x"
- | Names.Name x -> x
+ | Anonymous -> Id.of_string "x"
+ | Name x -> x
(* TODO: finish Rec caes *)
let ids_of_glob_constr c =
@@ -722,7 +722,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect
(* we first (pseudo) understand [rt] and get back the computed evar_map *)
(* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed.
If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *)
- let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Pretyping.empty_lvar expected_type rt in
+ let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
let ctx, f = Evarutil.nf_evars_and_universes ctx in
(* then we map [rt] to replace the implicit holes by their values *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f277c563a..d12aa7f42 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -65,7 +65,7 @@ let functional_induction with_clean c princl pat =
(or f_rec, f_rect) i*)
let princ_name =
Indrec.make_elimination_ident
- (Label.to_id (con_label c'))
+ (Label.to_id (Constant.label c'))
(Tacticals.elimination_sort_of_goal g)
in
try
@@ -342,8 +342,8 @@ let error_error names e =
let generate_principle (evd:Evd.evar_map ref) pconstants on_error
is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof
- (continue_proof : int -> Names.constant array -> EConstr.constr array -> int ->
- Tacmach.tactic) : unit =
+ (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
+ Proof_type.tactic) : unit =
let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
@@ -446,7 +446,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
let generate_correction_proof_wf f_ref tcc_lemma_ref
is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
- (_: int) (_:Names.constant array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
+ (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic =
Functional_principles_proofs.prove_principle_for_gen
(f_ref,functional_ref,eq_ref)
tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation
@@ -899,14 +899,14 @@ let make_graph (f_ref:global_reference) =
in
l
| _ ->
- let id = Label.to_id (con_label c) in
+ let id = Label.to_id (Constant.label c) in
[(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
- let mp,dp,_ = repr_con c in
+ let mp,dp,_ = Constant.repr3 c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
+ (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index a82a8b360..33420d813 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -16,7 +16,7 @@ val functional_induction :
EConstr.constr ->
(EConstr.constr * EConstr.constr bindings) option ->
Tacexpr.or_and_intro_pattern option ->
- Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
+ Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
val make_graph : Globnames.global_reference -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8f62231ae..7558ac7ac 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -109,7 +109,7 @@ let const_of_id id =
try Constrintern.locate_reference princ_ref
with Not_found ->
CErrors.user_err ~hdr:"IndFun.const_of_id"
- (str "cannot find " ++ Nameops.pr_id id)
+ (str "cannot find " ++ Id.print id)
let def_of_const t =
match (Term.kind_of_term t) with
@@ -217,14 +217,14 @@ let with_full_print f a =
type function_info =
{
- function_constant : constant;
+ function_constant : Constant.t;
graph_ind : inductive;
- equation_lemma : constant option;
- correctness_lemma : constant option;
- completeness_lemma : constant option;
- rect_lemma : constant option;
- rec_lemma : constant option;
- prop_lemma : constant option;
+ equation_lemma : Constant.t option;
+ correctness_lemma : Constant.t option;
+ completeness_lemma : Constant.t option;
+ rect_lemma : Constant.t option;
+ rec_lemma : Constant.t option;
+ prop_lemma : Constant.t option;
is_general : bool; (* Has this function been defined using general recursive definition *)
}
@@ -389,7 +389,7 @@ let update_Function finfo =
let add_Function is_general f =
- let f_id = Label.to_id (con_label f) in
+ let f_id = Label.to_id (Constant.label f) in
let equation_lemma = find_or_none (mk_equation_id f_id)
and correctness_lemma = find_or_none (mk_correct_id f_id)
and completeness_lemma = find_or_none (mk_complete_id f_id)
@@ -548,5 +548,5 @@ let compose_prod l b = prodn (List.length l) l b
type tcc_lemma_value =
| Undefined
- | Value of Constr.constr
+ | Value of Term.constr
| Not_needed
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index aa42b2ab9..6b40c9171 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -23,7 +23,7 @@ val array_get_start : 'a array -> 'a array
val id_of_name : Name.t -> Id.t
val locate_ind : Libnames.reference -> inductive
-val locate_constant : Libnames.reference -> constant
+val locate_constant : Libnames.reference -> Constant.t
val locate_with_msg :
Pp.std_ppcmds -> (Libnames.reference -> 'a) ->
Libnames.reference -> 'a
@@ -70,21 +70,21 @@ val with_full_print : ('a -> 'b) -> 'a -> 'b
type function_info =
{
- function_constant : constant;
+ function_constant : Constant.t;
graph_ind : inductive;
- equation_lemma : constant option;
- correctness_lemma : constant option;
- completeness_lemma : constant option;
- rect_lemma : constant option;
- rec_lemma : constant option;
- prop_lemma : constant option;
+ equation_lemma : Constant.t option;
+ correctness_lemma : Constant.t option;
+ completeness_lemma : Constant.t option;
+ rect_lemma : Constant.t option;
+ rec_lemma : Constant.t option;
+ prop_lemma : Constant.t option;
is_general : bool;
}
-val find_Function_infos : constant -> function_info
+val find_Function_infos : Constant.t -> function_info
val find_Function_of_graph : inductive -> function_info
(* WARNING: To be used just after the graph definition !!! *)
-val add_Function : bool -> constant -> unit
+val add_Function : bool -> Constant.t -> unit
val update_Function : function_info -> unit
@@ -123,5 +123,5 @@ val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
type tcc_lemma_value =
| Undefined
- | Value of Constr.constr
+ | Value of Term.constr
| Not_needed
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8152e181a..ebdb490e3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -218,7 +218,7 @@ let rec generate_fresh_id x avoid i =
\end{enumerate}
*)
-let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic =
+let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Proof_type.tactic =
fun g ->
(* first of all we recreate the lemmas types to be used as predicates of the induction principle
that is~:
@@ -342,7 +342,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
in
(* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *)
(
- tclTHENSEQ
+ tclTHENLIST
[
observe_tac("h_intro_patterns ") (let l = (List.nth intro_pats (pred i)) in
match l with
@@ -415,7 +415,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
in
(params_bindings@lemmas_bindings)
in
- tclTHENSEQ
+ tclTHENLIST
[
observe_tac "principle" (Proofview.V82.of_tactic (assert_by
(Name principle_id)
@@ -468,7 +468,7 @@ let tauto =
let rec intros_with_rewrite g =
observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
-and intros_with_rewrite_aux : tactic =
+and intros_with_rewrite_aux : Proof_type.tactic =
fun g ->
let eq_ind = make_eq () in
let sigma = project g in
@@ -480,16 +480,16 @@ and intros_with_rewrite_aux : tactic =
if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
then
let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
+ tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g))
- then tclTHENSEQ[
+ then tclTHENLIST[
Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]);
tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) )))
(pf_ids_of_hyps g);
intros_with_rewrite
] g
else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g))
- then tclTHENSEQ[
+ then tclTHENLIST[
Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]);
tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) )))
(pf_ids_of_hyps g);
@@ -498,7 +498,7 @@ and intros_with_rewrite_aux : tactic =
else if isVar sigma args.(1)
then
let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
+ tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
generalize_dependent_of (destVar sigma args.(1)) id;
tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
intros_with_rewrite
@@ -507,7 +507,7 @@ and intros_with_rewrite_aux : tactic =
else if isVar sigma args.(2)
then
let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
+ tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
generalize_dependent_of (destVar sigma args.(2)) id;
tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
intros_with_rewrite
@@ -516,7 +516,7 @@ and intros_with_rewrite_aux : tactic =
else
begin
let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENSEQ[
+ tclTHENLIST[
Proofview.V82.of_tactic (Simple.intro id);
tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
intros_with_rewrite
@@ -525,12 +525,12 @@ and intros_with_rewrite_aux : tactic =
| Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
- tclTHENSEQ[
+ tclTHENLIST[
Proofview.V82.of_tactic (simplest_case v);
intros_with_rewrite
] g
| LetIn _ ->
- tclTHENSEQ[
+ tclTHENLIST[
Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
@@ -542,10 +542,10 @@ and intros_with_rewrite_aux : tactic =
] g
| _ ->
let id = pf_get_new_id (Id.of_string "y") g in
- tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g
+ tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g
end
| LetIn _ ->
- tclTHENSEQ[
+ tclTHENLIST[
Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
@@ -562,7 +562,7 @@ let rec reflexivity_with_destruct_cases g =
try
match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with
| Case(_,_,v,_) ->
- tclTHENSEQ[
+ tclTHENLIST[
Proofview.V82.of_tactic (simplest_case v);
Proofview.V82.of_tactic intros;
observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
@@ -582,7 +582,7 @@ let rec reflexivity_with_destruct_cases g =
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
else if Equality.injectable (pf_env g) (project g) t1 t2
- then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g
+ then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g
else tclIDTAC g
| _ -> tclIDTAC g
)
@@ -629,7 +629,7 @@ let rec reflexivity_with_destruct_cases g =
*)
-let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
+let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.tactic =
fun g ->
(* We compute the types of the different mutually recursive lemmas
in $\zeta$ normal form
@@ -673,7 +673,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
using [f_equation] if it is recursive (that is the graph is infinite
or unfold if the graph is finite
*)
- let rewrite_tac j ids : tactic =
+ let rewrite_tac j ids : Proof_type.tactic =
let graph_def = graphs.(j) in
let infos =
try find_Function_infos (fst (destConst (project g) funcs.(j)))
@@ -686,7 +686,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
try Option.get (infos).equation_lemma
with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.")
in
- tclTHENSEQ[
+ tclTHENLIST[
tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
(* Don't forget to $\zeta$ normlize the term since the principles
@@ -722,7 +722,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
end
in
let this_branche_ids = List.nth intro_pats (pred i) in
- tclTHENSEQ[
+ tclTHENLIST[
(* we expand the definition of the function *)
observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
(* introduce hypothesis with some rewrite *)
@@ -735,7 +735,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
let params_names = fst (List.chop princ_infos.nparams args_names) in
let open EConstr in
let params = List.map mkVar params_names in
- tclTHENSEQ
+ tclTHENLIST
[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
observe_tac "h_generalize"
(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
@@ -807,7 +807,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
in
Array.iteri
(fun i f_as_constant ->
- let f_id = Label.to_id (con_label (fst f_as_constant)) in
+ let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
(*i The next call to mk_correct_id is valid since we are constructing the lemma
Ensures by: obvious
i*)
@@ -872,7 +872,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
in
Array.iteri
(fun i f_as_constant ->
- let f_id = Label.to_id (con_label (fst f_as_constant)) in
+ let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
(*i The next call to mk_complete_id is valid since we are constructing the lemma
Ensures by: obvious
i*)
@@ -923,7 +923,7 @@ let revert_graph kn post_tac hid g =
| None -> tclIDTAC g
| Some f_complete ->
let f_args,res = Array.chop (Array.length args - 1) args in
- tclTHENSEQ
+ tclTHENLIST
[
Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
thin [hid];
@@ -953,7 +953,7 @@ let revert_graph kn post_tac hid g =
\end{enumerate}
*)
-let functional_inversion kn hid fconst f_correct : tactic =
+let functional_inversion kn hid fconst f_correct : Proof_type.tactic =
fun g ->
let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in
let sigma = project g in
@@ -968,7 +968,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
((fun hid -> tclIDTAC),f_args,args.(1))
| _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
in
- tclTHENSEQ[
+ tclTHENLIST [
pre_tac hid;
Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
thin [hid];
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 290d0bb91..c75f7f868 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -893,7 +893,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
locate_constant f_ref in
try find_Function_infos (kn_of_id id)
with Not_found ->
- user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme")
+ user_err ~hdr:"indfun" (Id.print id ++ str " has no functional scheme")
(** [merge id1 id2 args1 args2 id] builds and declares a new inductive
type called [id], representing the merged graphs of both graphs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index bd74d2cf6..20abde82f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -77,7 +77,7 @@ let def_of_const t =
| _ -> raise Not_found)
with Not_found ->
anomaly (str "Cannot find definition of constant " ++
- (Id.print (Label.to_id (con_label (fst sp)))) ++ str ".")
+ (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".")
)
|_ -> assert false
@@ -172,7 +172,7 @@ let simpl_iter clause =
clause
(* Others ugly things ... *)
-let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
+let (value_f:Term.constr list -> global_reference -> Term.constr) =
let open Term in
fun al fterm ->
let rev_x_id_l =
@@ -204,7 +204,7 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
it_mkLambda_or_LetIn body context
-let (declare_f : Id.t -> logical_kind -> Constr.constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) =
fun f_id kind input_type fterm_ref ->
declare_fun f_id kind (value_f input_type fterm_ref);;
@@ -313,7 +313,7 @@ let check_not_nested sigma forbidden e =
| Var x ->
if Id.List.mem x forbidden
then user_err ~hdr:"Recdef.check_not_nested"
- (str "check_not_nested: failure " ++ pr_id x)
+ (str "check_not_nested: failure " ++ Id.print x)
| Meta _ | Evar _ | Sort _ -> ()
| Cast(e,_,t) -> check_not_nested e;check_not_nested t
| Prod(_,t,b) -> check_not_nested t;check_not_nested b
@@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
| Lambda(n,t,b) ->
begin
@@ -458,7 +458,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
jinfo.otherS () expr_info continuation_tac expr_info g
with e when CErrors.noncritical e ->
- user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+ user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
end
| Case(ci,t,a,l) ->
begin
@@ -683,7 +683,7 @@ let pf_typel l tac =
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 sigma -> tactic * Id.t list =
+ Id.t list -> constr -> goal Evd.sigma -> tactic * Id.t list =
fun not_on_hyp expr g ->
let hyps = pf_hyps g in
let to_revert =
@@ -691,7 +691,7 @@ let mkDestructEq :
(fun decl ->
let open Context.Named.Declaration in
let id = get_id decl in
- if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) expr (get_type decl))
+ 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
@@ -850,7 +850,7 @@ let rec prove_le g =
try
let matching_fun =
pf_is_matching g
- (Pattern.PApp(Pattern.PRef (reference_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in
+ (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in
let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
in
let y =
@@ -870,7 +870,7 @@ let rec make_rewrite_list expr_info max = function
| [] -> tclIDTAC
| (_,p,hp)::l ->
observe_tac (str "make_rewrite_list") (tclTHENS
- (observe_tac (str "rewrite heq on " ++ pr_id p ) (
+ (observe_tac (str "rewrite heq on " ++ Id.print p ) (
(fun g ->
let sigma = project g in
let t_eq = compute_renamed_type g (mkVar hp) in
@@ -965,7 +965,7 @@ let rec destruct_hex expr_info acc l =
onNthHypId 1 (fun hp ->
onNthHypId 2 (fun p ->
observe_tac
- (str "destruct_hex after " ++ pr_id hp ++ spc () ++ pr_id p)
+ (str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p)
(destruct_hex expr_info ((v,p,hp)::acc) l)
)
)
@@ -1457,7 +1457,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
let (com_eqn : int -> Id.t ->
global_reference -> global_reference -> global_reference
- -> Constr.constr -> unit) =
+ -> Term.constr -> unit) =
fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
let open CVars in
let opacity =
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-22 15:26:36 +0000