Correction de la premiere partie du #1278 (but non referme en cas d'echec)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9372 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 4 deletions

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 89ebb75a9..8ad2e72bb 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -405,11 +405,26 @@ let generate_functional_principle
   let (id,(entry,g_kind,hook)) =
     build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook 
   in
+  (* Pr  1278 :
+     Don't forget to close the goal if an error is raised !!!!
+  *) 
   save false new_princ_name entry g_kind hook
-  with 
-    | Defining_principle _ as e -> raise e
-    | e -> raise (Defining_principle e)
-
+  with e -> 
+    begin
+      begin 
+	try 
+	  let id = Pfedit.get_current_proof_name () in 
+	  let s = string_of_id id in 
+	  let n = String.length "___________princ_________" in
+	  if String.length s >= n 
+	  then if String.sub s 0 n = "___________princ_________" 
+	  then Pfedit.delete_current_proof ()
+	  else ()
+	  else ()
+	with _ -> ()
+      end;
+      raise (Defining_principle e)
+    end
 (*   defined  () *)