summaryrefslogtreecommitdiff
path: root/plugins/funind/invfun.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/invfun.ml')
-rw-r--r--plugins/funind/invfun.ml32
1 files changed, 15 insertions, 17 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index bed95740..ad11f853 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -23,7 +23,7 @@ open Tacticals
open Tactics
open Indfun_common
open Tacmach
-open Misctypes
+open Tactypes
open Termops
open Context.Rel.Declaration
@@ -67,7 +67,7 @@ let observe_tac s tac g =
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
Environ.empty_env
- Evd.empty
+ (Evd.from_env Environ.empty_env)
let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
@@ -81,7 +81,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
let make_eq () =
try
- EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
+ EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ()))
with _ -> assert false
@@ -102,9 +102,9 @@ let generate_type evd g_to_f f graph i =
let evd',graph =
Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph)))
in
- let graph = EConstr.of_constr graph in
evd:=evd';
- let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+ let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
+ evd := sigma;
let ctxt,_ = decompose_prod_assum !evd graph_arity in
let fun_ctxt,res_type =
match ctxt with
@@ -172,7 +172,6 @@ let find_induction_principle evd f =
| None -> raise Not_found
| Some rect_lemma ->
let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in
- let rect_lemma = EConstr.of_constr rect_lemma in
let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
evd:=evd';
rect_lemma,typ
@@ -240,7 +239,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
List.map
(fun decl ->
List.map
- (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id))
+ (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id))
(generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
)
branches
@@ -258,7 +257,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
List.fold_right
(fun {CAst.v=pat} acc ->
match pat with
- | IntroNaming (IntroIdentifier id) -> id::acc
+ | IntroNaming (Namegen.IntroIdentifier id) -> id::acc
| _ -> anomaly (Pp.str "Not an identifier.")
)
(List.nth intro_pats (pred i))
@@ -513,7 +512,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
intros_with_rewrite
] g
end
- | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
+ | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) ->
Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENLIST[
@@ -771,7 +770,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
graphs_constr.(i) <- graph;
let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
- let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in
+ let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
+ evd := sigma;
let type_of_lemma = nf_zeta type_of_lemma in
observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
type_of_lemma,type_info
@@ -818,13 +818,12 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))));
- (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+ (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
let finfo = find_Function_infos (fst f_as_constant) in
(* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
- let lem_cst_constr = EConstr.of_constr lem_cst_constr in
- let (lem_cst,_) = destConst !evd lem_cst_constr in
+ let (lem_cst,_) = destConst !evd lem_cst_constr in
update_Function {finfo with correctness_lemma = Some lem_cst};
)
@@ -880,12 +879,11 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i)))) ;
- (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+ (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
let finfo = find_Function_infos (fst f_as_constant) in
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
- let lem_cst_constr = EConstr.of_constr lem_cst_constr in
- let (lem_cst,_) = destConst !evd lem_cst_constr in
+ let (lem_cst,_) = destConst !evd lem_cst_constr in
update_Function {finfo with completeness_lemma = Some lem_cst}
)
funs)
@@ -969,7 +967,7 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic =
Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
- Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
+ Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid));
(fun g ->
let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
tclMAP (revert_graph kn pre_tac) (hid::new_ids) g
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 23:34:41 +0000