diff options
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 3 | ||||
-rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 4 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 8 |
7 files changed, 14 insertions, 11 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f0c7b5a7f..714192f53 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -988,7 +988,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (mk_equation_id f_id) (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) (lemma_type, (*FIXME*) Univ.ContextSet.empty) - (fun _ _ -> ()); + (Future.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); Lemmas.save_proof (Vernacexpr.Proved(false,None)) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a8876c75b..65a262707 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -290,7 +290,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") [] in - let hook = hook new_principle_type in + let hook = Future.mk_hook (hook new_principle_type) in begin Lemmas.start_proof new_princ_name @@ -305,7 +305,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - get_proof_clean true,Ephemeron.create hook + get_proof_clean true, Ephemeron.create hook end diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 70a892a3b..8c8d7a667 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -352,7 +352,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in Command.do_definition fname (Decl_kinds.Global,(*FIXME*)false,Decl_kinds.Definition) - bl None body (Some ret_type) (fun _ _ -> ()) + bl None body (Some ret_type) (Future.mk_hook (fun _ _ -> ())) | _ -> Command.do_fixpoint Global false(*FIXME*) fixpoint_exprl diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 0d1e600ee..b923260c2 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -147,6 +147,7 @@ let get_locality = function | Global -> false let save with_clean id const (locality,_,kind) hook = + let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in @@ -160,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Pfedit.delete_current_proof (); - Ephemeron.iter_opt hook (fun f -> f l r); + Ephemeron.iter_opt hook (fun f -> Future.call_hook fix_exn f l r); definition_message id diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 6e8b79a6b..3fafeadc1 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val const_of_id: Id.t -> constant val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr -val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> +val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> unit Tacexpr.declaration_hook Ephemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d5640798e..9558923f6 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1080,7 +1080,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Lemmas.start_proof lem_id (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) - (fun _ _ -> ()); + (Future.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); @@ -1133,7 +1133,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Lemmas.start_proof lem_id (Decl_kinds.Global,false(*FIXME*),(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i), (*FIXME*)Univ.ContextSet.empty) - (fun _ _ -> ()); + (Future.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 439014361..08d8ca391 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1320,7 +1320,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) (gls_type, ctx) - hook; + (Future.mk_hook hook); if Indfun_common.is_strict_tcc () then ignore (by (Proofview.V82.tactic (tclIDTAC))) @@ -1415,7 +1415,9 @@ let (com_eqn : int -> Id.t -> let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in (Lemmas.start_proof eq_name (Global, false, Proof Lemma) - ~sign:(Environ.named_context_val env) (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) (fun _ _ -> ()); + ~sign:(Environ.named_context_val env) + (equation_lemma_type, (*FIXME*)Univ.ContextSet.empty) + (Future.mk_hook (fun _ _ -> ())); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> @@ -1535,5 +1537,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - ctx hook) + ctx (Future.mk_hook hook)) () |