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

3 files changed, 8 insertions, 19 deletions

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