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 | 11 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
6 files changed, 14 insertions, 13 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 6913b40ea3..15e2843981 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -982,7 +982,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (mk_equation_id f_id) (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) lemma_type - (fun _ _ -> ()); + None; Pfedit.by (prove_replacement); Lemmas.save_named false diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index efed9a8560..a01039eb0b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -329,7 +329,7 @@ let generate_functional_principle id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in let names = ref [new_princ_name] in - let hook new_principle_type _ _ = + let hook new_principle_type = Some (fun _ _ -> if sorts = None then (* let id_of_f = Label.to_id (con_label f) in *) @@ -357,10 +357,11 @@ let generate_functional_principle names := name :: !names in register_with_sort InProp; - register_with_sort InSet + register_with_sort InSet) in let (id,(entry,g_kind,hook)) = - build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook + build_functional_principle interactive_proof old_princ_type new_sorts funs i + proof_tac hook in (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! @@ -517,7 +518,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis this_block_funs 0 (prove_princ_for_struct false 0 (Array.of_list funs)) - (fun _ _ _ -> ()) + (fun _ -> None) with e when Errors.noncritical e -> begin begin @@ -591,7 +592,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis this_block_funs !i (prove_princ_for_struct false !i (Array.of_list funs)) - (fun _ _ _ -> ()) + (fun _ -> None) in const with Found_type i -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 91badbfd76..d1fa16c0a9 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,Decl_kinds.Definition) - bl None body (Some ret_type) (fun _ _ -> ()) + bl None body (Some ret_type) None | _ -> Command.do_fixpoint Global fixpoint_exprl diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 4d26c4f533..827747c6b8 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -161,7 +161,7 @@ let save with_clean id const (locality,kind) hook = (locality, ConstRef kn) in if with_clean then Pfedit.delete_current_proof (); - hook l r; + Option.default (fun _ _ -> ()) hook l r; definition_message id diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 7d14d1408c..7c70815a68 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1061,7 +1061,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Lemmas.start_proof lem_id (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) - (fun _ _ -> ()); + None; Pfedit.by (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)); @@ -1112,7 +1112,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Lemmas.start_proof lem_id (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) - (fun _ _ -> ()); + None; Pfedit.by (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 68b291ff96..e6f6826357 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1313,7 +1313,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma) sign gls_type - hook ; + (Some hook) ; if Indfun_common.is_strict_tcc () then by (tclIDTAC) @@ -1406,7 +1406,7 @@ 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 (start_proof eq_name (Global, Proof Lemma) - (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ()); + (Environ.named_context_val env) equation_lemma_type None; by (start_equation f_ref terminate_ref (fun x -> @@ -1523,6 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - hook) + (Some hook)) () |