diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/invfun.ml | 49 |
1 files changed, 21 insertions, 28 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e4695792be..b92a8daf39 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1023,6 +1023,7 @@ let do_save () = Lemmas.save_named false *) let derive_correctness make_scheme functional_induction (funs: constant list) (graphs:inductive list) = + let previous_state = States.freeze () in let funs = Array.of_list funs and graphs = Array.of_list graphs in let funs_constr = Array.map mkConst funs in try @@ -1064,22 +1065,21 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.iteri (fun i f_as_constant -> let f_id = id_of_label (con_label f_as_constant) in - Lemmas.start_proof - (*i The next call to mk_correct_id is valid since we are constructing the lemma + (*i The next call to mk_correct_id is valid since we are constructing the lemma Ensures by: obvious - i*) - (mk_correct_id f_id) + i*) + let lem_id = mk_correct_id f_id in + Lemmas.start_proof lem_id (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); - Pfedit.by (observe_tac ("prove correctness ("^(string_of_id f_id)^")") (proving_tac i)); + Pfedit.by + (observe_tac ("prove correctness ("^(string_of_id f_id)^")") + (proving_tac i)); do_save (); let finfo = find_Function_infos f_as_constant in - update_Function - {finfo with - correctness_lemma = Some (destConst (Constrintern.global_reference (mk_correct_id f_id))) - } - + let lem_cst = destConst (Constrintern.global_reference lem_id) in + update_Function {finfo with correctness_lemma = Some lem_cst} ) funs; let lemmas_types_infos = @@ -1116,34 +1116,27 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.iteri (fun i f_as_constant -> let f_id = id_of_label (con_label f_as_constant) in - Lemmas.start_proof - (*i The next call to mk_complete_id is valid since we are constructing the lemma + (*i The next call to mk_complete_id is valid since we are constructing the lemma Ensures by: obvious - i*) - (mk_complete_id f_id) + i*) + let lem_id = mk_complete_id f_id in + Lemmas.start_proof lem_id (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) (fst lemmas_types_infos.(i)) (fun _ _ -> ()); - Pfedit.by (observe_tac ("prove completeness ("^(string_of_id f_id)^")") (proving_tac i)); + Pfedit.by + (observe_tac ("prove completeness ("^(string_of_id f_id)^")") + (proving_tac i)); do_save (); let finfo = find_Function_infos f_as_constant in - update_Function - {finfo with - completeness_lemma = Some (destConst (Constrintern.global_reference (mk_complete_id f_id))) - } + let lem_cst = destConst (Constrintern.global_reference lem_id) in + update_Function {finfo with completeness_lemma = Some lem_cst} ) funs; with e -> (* In case of problem, we reset all the lemmas *) - (*i The next call to mk_correct_id is valid since we are erasing the lemmas - Ensures by: obvious - i*) - let first_lemma_id = - let f_id = id_of_label (con_label funs.(0)) in - - mk_correct_id f_id - in - (try Backtrack.reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ()); + Pfedit.delete_all_proofs (); + States.unfreeze previous_state; raise e |