Report de la révision r9605 de la branche v8.1 vers le trunk (abstract récupère toutes les exceptions)

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

1 files changed, 25 insertions, 27 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 282e417c3..9e25055e9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2464,36 +2464,34 @@ let abstract_subproof name tac gls =
   let sign,secsign = 
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) -> 
-	 if mem_named_context id current_sign &
-           interpretable_as_section_decl (Sign.lookup_named id current_sign) d
-         then (s1,push_named_context_val d s2)
-	 else (add_named_decl d s1,s2)) 
+	if mem_named_context id current_sign &
+          interpretable_as_section_decl (Sign.lookup_named id current_sign) d
+        then (s1,push_named_context_val d s2)
+	else (add_named_decl d s1,s2)) 
       global_sign (empty_named_context,empty_named_context_val) in
   let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
-  if occur_existential concl then
-    error "\"abstract\" cannot handle existentials";
-  let lemme =
-    start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
-    let _,(const,kind,_) =
-      try
-	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
-	let r = cook_proof () in 
-	delete_current_proof (); r
-      with 
-	  e when catchable_exception e -> 
-	    (delete_current_proof(); raise e)
-	| FailError (0,_) as e -> 
-	    (delete_current_proof(); raise e)
-    in   (* Faudrait un peu fonctionnaliser cela *)
-    let cd = Entries.DefinitionEntry const in
-    let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in
-    constr_of_global (ConstRef con)
-  in
-  exact_no_check 
-    (applist (lemme, 
-              List.rev (Array.to_list (instance_from_named_context sign))))
-    gls
+    if occur_existential concl then
+      error "\"abstract\" cannot handle existentials";
+    let lemme =
+      start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
+      let _,(const,kind,_) =
+	try
+	  by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
+	  let r = cook_proof () in 
+	    delete_current_proof (); r
+	with 
+	    e ->
+	      (delete_current_proof(); raise e)
+      in   (* Faudrait un peu fonctionnaliser cela *)
+      let cd = Entries.DefinitionEntry const in
+      let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in
+	constr_of_global (ConstRef con)
+    in
+      exact_no_check 
+	(applist (lemme, 
+		 List.rev (Array.to_list (instance_from_named_context sign))))
+	gls
 
 let tclABSTRACT name_op tac gls = 
   let s = match name_op with