Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

correct abort in Function when a proof of inversion fails

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15239 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit fe83af687a7cec576063c4b5c4e94d8ad33fca7d 1 parent 83b342c
letouzey authored Maxime Dénès committed
View
49 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
View
2  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
View
13 toplevel/vernacentries.ml
@@ -764,14 +764,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 *)
View
12 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
Please sign in to comment.
Something went wrong with that request. Please try again.