From 635bdc1ca5754778c2af4f013fa8c327e7197bf2 Mon Sep 17 00:00:00 2001
From: jforest
Date: Mon, 13 Nov 2006 10:32:27 +0000
Subject: 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
---
 contrib/funind/functional_principles_types.ml | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 89ebb75a96..8ad2e72bbf 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  () *)
 
 
-- 
cgit v1.2.3