aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml87
-rw-r--r--plugins/funind/functional_principles_proofs.mli7
-rw-r--r--plugins/funind/functional_principles_types.ml30
-rw-r--r--plugins/funind/functional_principles_types.mli7
-rw-r--r--plugins/funind/g_indfun.ml431
-rw-r--r--plugins/funind/glob_term_to_relation.ml16
-rw-r--r--plugins/funind/glob_term_to_relation.mli1
-rw-r--r--plugins/funind/glob_termops.ml54
-rw-r--r--plugins/funind/glob_termops.mli8
-rw-r--r--plugins/funind/indfun.ml40
-rw-r--r--plugins/funind/indfun.mli3
-rw-r--r--plugins/funind/indfun_common.ml25
-rw-r--r--plugins/funind/indfun_common.mli23
-rw-r--r--plugins/funind/invfun.ml92
-rw-r--r--plugins/funind/merge.ml17
-rw-r--r--plugins/funind/recdef.ml57
-rw-r--r--plugins/funind/recdef.mli2
-rw-r--r--plugins/funind/vo.itarget1
18 files changed, 253 insertions, 248 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 434fb14a6..ef894b239 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,3 +1,4 @@
+open API
open Printer
open CErrors
open Util
@@ -105,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
}
@@ -397,7 +398,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
then tclIDTAC g
else
match eq_ids with
- | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
+ | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property.");
| eq_id::eq_ids ->
tclTHEN
(tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
@@ -605,7 +606,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
pr_leconstr_env (pf_env g') (project g') new_term_value_eq
);
- anomaly (Pp.str "cannot compute new term value")
+ anomaly (Pp.str "cannot compute new term value.")
in
let fun_body =
mkLambda(Anonymous,
@@ -687,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 =
@@ -707,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
@@ -838,7 +839,7 @@ let build_proof
h_reduce_with_zeta Locusops.onConcl;
build_proof do_finalize new_infos
] g
- | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
+ | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
and build_proof do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
@@ -944,7 +945,7 @@ let generalize_non_dep hyp g =
((* observe_tac "thin" *) (thin to_revert))
g
-let id_of_decl = RelDecl.get_name %> Nameops.out_name
+let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id
let var_of_decl = id_of_decl %> mkVar
let revert idl =
tclTHEN
@@ -981,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
@@ -1018,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*)
@@ -1032,7 +1033,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
{finfos with
equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
ConstRef c -> c
- | _ -> CErrors.anomaly (Pp.str "Not a constant")
+ | _ -> CErrors.anomaly (Pp.str "Not a constant.")
)
}
| _ -> ()
@@ -1127,11 +1128,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
)
in
observe (str "full_params := " ++
- prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+ prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
full_params
);
observe (str "princ_params := " ++
- prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+ prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
princ_params
);
observe (str "fbody_with_full_params := " ++
@@ -1158,7 +1159,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(fun i types ->
let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in
{ idx = idxs.(i) - fix_offset;
- name = Nameops.out_name (fresh_id names.(i));
+ name = Nameops.Name.get_id (fresh_id names.(i));
types = types;
offset = fix_offset;
nb_realargs =
@@ -1181,7 +1182,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
let app_f = mkApp(f,first_args) in
let pte_args = (Array.to_list first_args)@[app_f] in
- let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in
+ let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in
let body_with_param,num =
let body = get_body fnames.(i) in
let body_with_full_params =
@@ -1208,9 +1209,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
num_in_block = num
}
in
-(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++ *)
+(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *)
(* str " to " ++ Ppconstr.pr_id info.name); *)
- (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info)
+ (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info)
)
0
(Id.Map.empty,[])
@@ -1241,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)));
@@ -1255,11 +1256,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
try
let pte =
try destVar (project gl) pte
- with DestKO -> anomaly (Pp.str "Property is not a variable")
+ with DestKO -> anomaly (Pp.str "Property is not a variable.")
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 *)
@@ -1278,13 +1279,13 @@ 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
full_params
(fix_info.idx + List.length princ_params)
- (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params))
+ (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params))
(all_funs.(fix_info.num_in_block))
fix_info.num_in_block
all_funs
@@ -1321,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 *)
@@ -1342,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
@@ -1401,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; *)
@@ -1456,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)));
@@ -1481,7 +1482,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
tclCOMPLETE(
Eauto.eauto_with_bases
(true,5)
- [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+ [(fun _ sigma -> (sigma, Lazy.force refl_equal))]
[Hints.Hint_db.empty empty_transparent_state false]
)
)
@@ -1563,17 +1564,17 @@ let prove_principle_for_gen
| _ -> assert false
in
(* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
- let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in
+ let subst_constrs = List.map (get_name %> Nameops.Name.get_id %> mkVar) (pre_rec_arg@princ_info.params) in
let relation = substl subst_constrs relation in
let input_type = substl subst_constrs rec_arg_type in
- let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
+ let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in
let acc_rec_arg_id =
- Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
+ Nameops.Name.get_id (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
in
let revert l =
tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
in
- let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
+ let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
let prove_rec_arg_acc g =
((* observe_tac "prove_rec_arg_acc" *)
(tclCOMPLETE
@@ -1591,7 +1592,7 @@ let prove_principle_for_gen
)
g
in
- let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
+ let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in
let lemma =
match !tcc_lemma_ref with
| Undefined -> user_err Pp.(str "No tcc proof !!")
@@ -1616,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);
@@ -1635,11 +1636,11 @@ let prove_principle_for_gen
]
gls
in
- tclTHENSEQ
+ tclTHENLIST
[
observe_tac "start_tac" start_tac;
h_intros
- (List.rev_map (get_name %> Nameops.out_name)
+ (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
@@ -1677,14 +1678,14 @@ let prove_principle_for_gen
in
let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in
let predicates_names =
- List.map (get_name %> Nameops.out_name) princ_info.predicates
+ List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
in
let pte_info =
{ proving_tac =
(fun eqs ->
(* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *)
-(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *)
-(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *)
+(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
+(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
(* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *)
(* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *)
@@ -1693,7 +1694,7 @@ let prove_principle_for_gen
is_mes acc_inv fix_id
(!tcc_list@(List.map
- (get_name %> Nameops.out_name)
+ (get_name %> Nameops.Name.get_id)
(princ_info.args@princ_info.params)
)@ ([acc_rec_arg_id])) eqs
)
@@ -1722,7 +1723,7 @@ let prove_principle_for_gen
(* observe_tac "instanciate_hyps_with_args" *)
(instanciate_hyps_with_args
make_proof
- (List.map (get_name %> Nameops.out_name) princ_info.branches)
+ (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
(List.rev args_ids)
)
gl'
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 61752aa33..5bb288678 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,19 +1,20 @@
+open API
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 18d63dd94..70245a8b1 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,3 +1,4 @@
+open API
open Printer
open CErrors
open Util
@@ -12,7 +13,6 @@ open Context.Rel.Declaration
open Indfun_common
open Functional_principles_proofs
open Misctypes
-open Sigma.Notations
module RelDecl = Context.Rel.Declaration
@@ -44,7 +44,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let id = Namegen.next_ident_away x avoid in
Hashtbl.add tbl id x;
RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
- | Anonymous -> anomaly (Pp.str "Anonymous property binder "))
+ | Anonymous -> anomaly (Pp.str "Anonymous property binder."))
in
let avoid = (Termops.ids_of_context env_with_params ) in
let princ_type_info =
@@ -62,7 +62,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
then List.tl args
else args
in
- Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl),
+ Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl),
Term.compose_prod real_args (mkSort new_sort))
in
let new_predicates =
@@ -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
@@ -185,11 +185,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
with
| Toberemoved ->
-(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
new_b, List.map pop binders_to_remove_from_b
| Toberemoved_with_rel (n,c) ->
-(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
end
@@ -214,11 +214,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
with
| Toberemoved ->
-(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
new_b, List.map pop binders_to_remove_from_b
| Toberemoved_with_rel (n,c) ->
-(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
end
@@ -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,17 +389,17 @@ 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")
+ anomaly (Pp.str "Anonymous fix.")
)
na
| _ -> [|const,0|]
@@ -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
@@ -669,11 +669,9 @@ let build_case_scheme fa =
let ind = first_fun_kn,funs_indexes in
(ind,Univ.Instance.empty)(*FIXME*),prop_sort
in
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma (scheme, sigma, _) =
+ let (sigma, scheme) =
Indrec.build_case_analysis_scheme_default env sigma ind sf
in
- let sigma = Sigma.to_evar_map sigma in
let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in
let sorts =
(fun (_,_,x) ->
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 45ad332fc..bb2b2d918 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Names
open Term
open Misctypes
@@ -17,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 *)
@@ -27,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 1db8be081..1258c9286 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "grammar/grammar.cma" i*)
+open API
+open Grammar_API
open Ltac_plugin
open Util
open Pp
@@ -22,26 +24,10 @@ open Pltac
DECLARE PLUGIN "recdef_plugin"
-let pr_binding prc = function
- | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
- | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
-
-let pr_bindings prc prlc = function
- | ImplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence prc l
- | ExplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
-let pr_with_bindings prc prlc (c,bl) =
- prc c ++ hv 0 (pr_bindings prc prlc bl)
-
let pr_fun_ind_using prc prlc _ opt_c =
match opt_c with
| None -> mt ()
- | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b)
+ | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
(* Duplication of printing functions because "'a with_bindings" is
(internally) not uniform in 'a: indeed constr_with_bindings at the
@@ -49,16 +35,12 @@ let pr_fun_ind_using prc prlc _ opt_c =
"constr with_bindings"; hence, its printer cannot be polymorphic in
(prc,prlc)... *)
-let pr_with_bindings_typed prc prlc (c,bl) =
- prc c ++
- hv 0 (pr_bindings prc prlc bl)
-
let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some b ->
- let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
- spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
+ let (_, b) = b (Global.env ()) Evd.empty in
+ spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
ARGUMENT EXTEND fun_ind_using
@@ -80,7 +62,6 @@ TACTIC EXTEND newfuninv
]
END
-
let pr_intro_as_pat _prc _ _ pat =
match pat with
| Some pat ->
@@ -185,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_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 68e097fe9..0e2ca4900 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,3 +1,4 @@
+open API
open Printer
open Pp
open Names
@@ -1115,7 +1116,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
else
CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
- | _ -> anomaly (Pp.str "Should not have an anonymous function here")
+ | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
(* We have renamed all the anonymous functions during alpha_renaming phase *)
end
@@ -1288,17 +1289,20 @@ let do_build_inductive
let t = EConstr.Unsafe.to_constr t in
evd,
Environ.push_named (LocalAssum (id,t))
- (* try *)
- (* Typing.e_type_of env evd (mkConstU c) *)
- (* with Not_found -> *)
- (* raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) *)
env
)
funnames
(Array.of_list funconstants)
(evd,Global.env ())
in
- let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
+ (* we solve and replace the implicits *)
+ let rta =
+ Array.mapi (fun i rt ->
+ let _,t = Typing.type_of env evd (EConstr.of_constr (mkConstU ((Array.of_list funconstants).(i)))) in
+ resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt
+ ) rta
+ in
+ let resa = Array.map (build_entry_lc env funnames_as_set []) rta in
let env_with_graphs =
let rel_arity i funargs = (* Rebuilding arities (with parameters) *)
let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list =
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 0cab5a6d3..7ad7de079 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -1,3 +1,4 @@
+open API
open Names
(*
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0361e8cb1..a7481370a 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,3 +1,4 @@
+open API
open Pp
open Glob_term
open CErrors
@@ -532,7 +533,7 @@ let rec are_unifiable_aux = function
else
let eqs' =
try (List.combine cpl1 cpl2) @ eqs
- with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux")
+ with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux.")
in
are_unifiable_aux eqs'
@@ -555,7 +556,7 @@ let rec eq_cases_pattern_aux = function
else
let eqs' =
try (List.combine cpl1 cpl2) @ eqs
- with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux")
+ with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux.")
in
eq_cases_pattern_aux eqs'
| _ -> raise NotUnifiable
@@ -578,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 =
@@ -707,3 +708,48 @@ let expand_as =
(loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
in
expand_as Id.Map.empty
+
+
+
+
+(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
+ *)
+
+exception Found of Evd.evar_info
+let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expected_type=Pretyping.WithoutTypeConstraint) env sigma rt =
+ let open Evd in
+ let open Evar_kinds in
+ (* 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, f = Evarutil.nf_evars_and_universes ctx in
+
+ (* then we map [rt] to replace the implicit holes by their values *)
+ let rec change rt =
+ match rt.CAst.v with
+ | GHole(ImplicitArg(grk,pk,bk),_,_) -> (* we only want to deal with implicit arguments *)
+ (
+ try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *)
+ Evd.fold (* to simulate an iter *)
+ (fun _ evi _ ->
+ match evi.evar_source with
+ | (loc_evi,ImplicitArg(gr_evi,p_evi,b_evi)) ->
+ if Globnames.eq_gr grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi
+ then raise (Found evi)
+ | _ -> ()
+ )
+ ctx
+ ();
+ (* the hole was not solved : we do nothing *)
+ rt
+ with Found evi -> (* we found the evar corresponding to this hole *)
+ match evi.evar_body with
+ | Evar_defined c ->
+ (* we just have to lift the solution in glob_term *)
+ Detyping.detype false [] env ctx (EConstr.of_constr (f c))
+ | Evar_empty -> rt (* the hole was not solved : we do nothing *)
+ )
+ | _ -> Glob_ops.map_glob_constr change rt
+ in
+ change rt
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 25d79582f..b6d2c4543 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,3 +1,4 @@
+open API
open Names
open Glob_term
open Misctypes
@@ -119,3 +120,10 @@ val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr
val expand_as : glob_constr -> glob_constr
+
+
+(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution
+ *)
+val resolve_and_replace_implicits :
+ ?flags:Pretyping.inference_flags ->
+ ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> glob_constr -> glob_constr
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 74c0eb4cc..d12aa7f42 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,3 +1,4 @@
+open API
open CErrors
open Util
open Names
@@ -11,7 +12,6 @@ open Glob_term
open Declarations
open Misctypes
open Decl_kinds
-open Sigma.Notations
module RelDecl = Context.Rel.Declaration
@@ -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
@@ -93,7 +93,7 @@ let functional_induction with_clean c princl pat =
in
let encoded_pat_as_patlist =
List.make (List.length args + List.length c_list - 1) None @ [pat] in
- List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
+ List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None))
(args@c_list) encoded_pat_as_patlist
in
let princ' = Some (princ,bindings) in
@@ -142,7 +142,7 @@ let rec abstract_glob_constr c = function
let interp_casted_constr_with_implicits env sigma impls c =
Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
- ~allow_patvar:false c
+ c
(*
Construct a fixpoint as a Glob_term
@@ -200,13 +200,13 @@ let is_rec names =
| GIf(b,_,lhs,rhs) ->
(lookup names b) || (lookup names lhs) || (lookup names rhs)
| GProd(na,_,t,b) | GLambda(na,_,t,b) ->
- lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
+ lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b
| GLetIn(na,b,t,c) ->
- lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c
+ lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c
| GLetTuple(nal,_,t,b) -> lookup names t ||
lookup
(List.fold_left
- (fun acc na -> Nameops.name_fold Id.Set.remove na acc)
+ (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc)
names
nal
)
@@ -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
@@ -734,7 +734,7 @@ let rec add_args id new_args = CAst.map (function
CAppExpl((None,r,None),new_args)
| _ -> b
end
- | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
+ | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
| CProdN(nal,b1) ->
CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
add_args id new_args b1)
@@ -782,9 +782,9 @@ let rec add_args id new_args = CAst.map (function
Miscops.map_cast_type (add_args id new_args) b2)
| CRecord pars ->
CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
- | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
- | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
- | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters")
+ | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
+ | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
+ | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
)
exception Stop of Constrexpr.constr_expr
@@ -826,7 +826,7 @@ let rec chop_n_arrow n t =
chop_n_arrow new_n t'
with Stop t -> t
end
- | _ -> anomaly (Pp.str "Not enough products")
+ | _ -> anomaly (Pp.str "Not enough products.")
let rec get_args b t : Constrexpr.local_binder_expr list *
@@ -856,7 +856,7 @@ let make_graph (f_ref:global_reference) =
| _ -> raise (UserError (None, str "Not a function reference") )
in
(match Global.body_of_constant_body c_body with
- | None -> error "Cannot build a graph over an axiom !"
+ | None -> error "Cannot build a graph over an axiom!"
| Some body ->
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -885,7 +885,7 @@ let make_graph (f_ref:global_reference) =
| Constrexpr.CLocalAssum (nal,_,_) ->
List.map
(fun (loc,n) -> CAst.make ?loc @@
- CRef(Libnames.Ident(loc, Nameops.out_name n),None))
+ CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
nal
| Constrexpr.CLocalPattern _ -> assert false
)
@@ -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 ba89fe4a7..33420d813 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,3 +1,4 @@
+open API
open Misctypes
val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
@@ -15,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 2476478ab..7558ac7ac 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,3 +1,4 @@
+open API
open Names
open Pp
open Libnames
@@ -108,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
@@ -216,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 *)
}
@@ -369,7 +370,7 @@ let in_Function : function_info -> Libobject.obj =
let find_or_none id =
try Some
- (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant")
+ (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
)
with Not_found -> None
@@ -388,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)
@@ -397,7 +398,7 @@ let add_Function is_general f =
and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
and graph_ind =
match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
- with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive")
+ with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
in
let finfos =
{ function_constant = f;
@@ -547,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 5ef8f05bb..6b40c9171 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,3 +1,4 @@
+open API
open Names
open Pp
@@ -22,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
@@ -69,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
@@ -122,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 d68bdc215..ebdb490e3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Ltac_plugin
open Declarations
open CErrors
@@ -26,31 +27,6 @@ open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
-(* Some pretty printing function for debugging purpose *)
-
-let pr_binding prc =
- function
- | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
- | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
-
-let pr_bindings prc prlc = function
- | ImplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence prc l
- | ExplicitBindings l ->
- brk (1,1) ++ str "with" ++ brk (1,1) ++
- pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
-
-let pr_with_bindings prc prlc (c,bl) =
- prc c ++ hv 0 (pr_bindings prc prlc bl)
-
-
-
-let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds =
- pr_with_bindings prc prc (c,bl)
-
(* The local debugging mechanism *)
(* let msgnl = Pp.msgnl *)
@@ -140,7 +116,7 @@ let generate_type evd g_to_f f graph i =
let ctxt,_ = decompose_prod_assum !evd graph_arity in
let fun_ctxt,res_type =
match ctxt with
- | [] | [_] -> anomaly (Pp.str "Not a valid context")
+ | [] | [_] -> anomaly (Pp.str "Not a valid context.")
| decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl
in
let rec args_from_decl i accu = function
@@ -242,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~:
@@ -292,7 +268,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(fun (_,pat) acc ->
match pat with
| IntroNaming (IntroIdentifier id) -> id::acc
- | _ -> anomaly (Pp.str "Not an identifier")
+ | _ -> anomaly (Pp.str "Not an identifier.")
)
(List.nth intro_pats (pred i))
[]
@@ -366,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
@@ -401,7 +377,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
Array.map
(fun ((_,(ctxt,concl))) ->
match ctxt with
- | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
+ | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.")
| hres::res::decl::ctxt ->
let res = EConstr.it_mkLambda_or_LetIn
(EConstr.it_mkProd_or_LetIn concl [hres;res])
@@ -421,7 +397,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let params_bindings,avoid =
List.fold_left2
(fun (bindings,avoid) decl p ->
- let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
+ let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
p::bindings,id::avoid
)
([],pf_ids_of_hyps g)
@@ -431,7 +407,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let lemmas_bindings =
List.rev (fst (List.fold_left2
(fun (bindings,avoid) decl p ->
- let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
+ let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
(nf_zeta p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
@@ -439,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)
@@ -492,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
@@ -504,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);
@@ -522,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
@@ -531,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
@@ -540,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
@@ -549,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
@@ -566,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
@@ -586,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
@@ -606,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
)
@@ -653,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
@@ -697,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)))
@@ -708,9 +684,9 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
then
let eq_lemma =
try Option.get (infos).equation_lemma
- with Option.IsNone -> anomaly (Pp.str "Cannot find 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
@@ -746,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 *)
@@ -759,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)]));
@@ -831,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*)
@@ -896,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*)
@@ -938,7 +914,7 @@ let revert_graph kn post_tac hid g =
let info =
try find_Function_of_graph ind'
with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
- anomaly (Pp.str "Cannot retrieve infos about a mutual block")
+ anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
in
(* if we can find a completeness lemma for this function
then we can come back to the functional form. If not, we do nothing
@@ -947,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];
@@ -977,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
@@ -992,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 b2c8489ce..c75f7f868 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -8,6 +8,7 @@
(* Merging of induction principles. *)
+open API
open Globnames
open Tactics
open Indfun_common
@@ -133,20 +134,6 @@ let prNamedRLDecl s lc =
prstr "\n";
end
-let showind (id:Id.t) =
- let cstrid = Constrintern.global_reference id in
- let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
- let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
- let u = EConstr.Unsafe.to_instance u in
- List.iter (fun decl ->
- print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
- prconstr (RelDecl.get_type decl); print_string "\n")
- ib1.mind_arity_ctxt;
- Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u));
- Array.iteri
- (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
- ib1.mind_user_lc
-
(** {2 Misc} *)
exception Found of int
@@ -906,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 2f9f70876..20abde82f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
+
module CVars = Vars
open Term
@@ -42,7 +44,6 @@ open Auto
open Eauto
open Indfun_common
-open Sigma.Notations
open Context.Rel.Declaration
(* Ugly things which should not be here *)
@@ -76,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)))))
+ (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".")
)
|_ -> assert false
@@ -95,7 +96,7 @@ let constant sl s = constr_of_global (find_reference sl s)
let const_of_ref = function
ConstRef kn -> kn
- | _ -> anomaly (Pp.str "ConstRef expected")
+ | _ -> anomaly (Pp.str "ConstRef expected.")
let nf_zeta env =
@@ -171,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 =
@@ -203,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);;
@@ -312,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
@@ -442,14 +443,14 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
travel jinfo new_continuation_tac
{expr_info with info = b; is_final=false} g
end
- | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
+ | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
| Prod _ ->
begin
try
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
@@ -457,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
@@ -486,7 +487,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
travel_args jinfo
expr_info.is_main_branch new_continuation_tac new_infos g
| Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
- | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info)
+ | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".")
end
| Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
| Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
@@ -682,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 =
@@ -690,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
@@ -700,11 +701,9 @@ let mkDestructEq :
observe_tclTHENLIST (str "mkDestructEq")
[Proofview.V82.of_tactic (generalize new_hyps);
(fun g2 ->
- let changefun patvars = { run = fun sigma ->
- let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
- let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2) in
- Sigma (c, sigma, p)
- } in
+ let changefun patvars 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);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
@@ -851,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 =
@@ -871,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
@@ -879,7 +878,7 @@ let rec make_rewrite_list expr_info max = function
let k_na,_,t = destProd sigma t_eq in
let _,_,t = destProd sigma t in
let def_na,_,_ = destProd sigma t in
- Nameops.out_name k_na,Nameops.out_name def_na
+ Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
in
Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
@@ -905,7 +904,7 @@ let make_rewrite expr_info l hp max =
let k_na,_,t = destProd sigma t_eq in
let _,_,t = destProd sigma t in
let def_na,_,_ = destProd sigma t in
- Nameops.out_name k_na,Nameops.out_name def_na
+ Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
in
observe_tac (str "general_rewrite_bindings")
(Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
@@ -966,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)
)
)
@@ -1165,7 +1164,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let f_id =
match f_name with
| Name f_id -> next_ident_away_in_goal f_id ids
- | Anonymous -> anomaly (Pp.str "Anonymous function")
+ | Anonymous -> anomaly (Pp.str "Anonymous function.")
in
let n_names_types,_ = decompose_lam_n sigma nb_args body1 in
let n_ids,ids =
@@ -1175,7 +1174,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
| Name id ->
let n_id = next_ident_away_in_goal id ids in
n_id::n_ids,n_id::ids
- | _ -> anomaly (Pp.str "anonymous argument")
+ | _ -> anomaly (Pp.str "anonymous argument.")
)
([],(f_id::ids))
n_names_types
@@ -1302,7 +1301,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| None ->
try add_suffix current_proof_name "_subproof"
with e when CErrors.noncritical e ->
- anomaly (Pp.str "open_new_goal with an unamed theorem")
+ anomaly (Pp.str "open_new_goal with an unamed theorem.")
in
let na = next_global_ident_away name [] in
if Termops.occur_existential sigma gls_type then
@@ -1313,7 +1312,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let na_global = Smartlocate.global_with_alias na_ref in
match na_global with
ConstRef c -> is_opaque_constant c
- | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
+ | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.")
in
let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
ref_ := Value (EConstr.Unsafe.to_constr lemma);
@@ -1357,7 +1356,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
(Proofview.V82.of_tactic e_assumption);
Eauto.eauto_with_bases
(true,5)
- [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+ [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))]
[Hints.Hint_db.empty empty_transparent_state false]
]
)
@@ -1458,13 +1457,13 @@ 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 =
match terminate_ref with
| ConstRef c -> is_opaque_constant c
- | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
+ | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
let (evmap, env) = Lemmas.get_current_context() in
let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 80f02e01c..e1a072799 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,4 +1,4 @@
-
+open API
(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
val tclUSER_if_not_mes :
diff --git a/plugins/funind/vo.itarget b/plugins/funind/vo.itarget
deleted file mode 100644
index 33c968302..000000000
--- a/plugins/funind/vo.itarget
+++ /dev/null
@@ -1 +0,0 @@
-Recdef.vo
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 18:22:14 +0000