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

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