diff options
| -rw-r--r-- | plugins/funind/invfun.ml | 49 | ||||
| -rw-r--r-- | toplevel/backtrack.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 13 | ||||
| -rw-r--r-- | toplevel/vernacentries.mli | 12 |
4 files changed, 29 insertions, 47 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e4695792b..b92a8daf3 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 diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index a84550a5d..24a056d73 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -167,7 +167,7 @@ let reset_initial () = let init_label = Lib.first_command_label in if Lib.current_command_label () = init_label then () else begin - if Pfedit.refining() then Pfedit.delete_all_proofs (); + Pfedit.delete_all_proofs (); Lib.reset_label init_label; Stack.clear history; Stack.push diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3652e2a6b..22ac6e90c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -745,14 +745,13 @@ let vernac_chdir = function (********************) (* State management *) -let abort_refine f x = - if Pfedit.refining() then delete_all_proofs (); - f x - (* used to be: error "Must save or abort current goal first" *) +let vernac_write_state file = + Pfedit.delete_all_proofs (); + States.extern_state file -let vernac_write_state file = abort_refine States.extern_state file - -let vernac_restore_state file = abort_refine States.intern_state file +let vernac_restore_state file = + Pfedit.delete_all_proofs (); + States.intern_state file (************) (* Commands *) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 66aa6c20a..a9d384ea0 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -23,13 +23,6 @@ val show_node : unit -> unit in the context of the current goal, as for instance in pcoq *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env -(*i - -(** this function is used to analyse the extra arguments in search commands. - It is used in pcoq. *) (*i anciennement: inside_outside i*) -val interp_search_restriction : search_restriction -> dir_path list * bool -i*) - type pcoq_hook = { start_proof : unit -> unit; solve : int -> unit; @@ -44,10 +37,7 @@ type pcoq_hook = { val set_pcoq_hook : pcoq_hook -> unit -(** This function makes sure that the function given in argument is preceded - by a command aborting all proofs if necessary. - It is used in pcoq. *) -val abort_refine : ('a -> unit) -> 'a -> unit;; +(** The main interpretation function of vernacular expressions *) val interp : Vernacexpr.vernac_expr -> unit |