Abstract: on échoue si le but contient des existentielles

(corrige un ug de EAuto with zarith)


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

1 files changed, 13 insertions, 10 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 08e35f50e2..c92d80641a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1689,15 +1689,17 @@ let abstract_subproof name tac gls =
   let env = Global.env() in
   let current_sign = Global.named_context()
   and global_sign = pf_hyps gls in
-  let sign = List.fold_right
-               (fun (id,_,_ as d) s -> 
-		  if mem_named_context id current_sign then s else add_named_decl d s) 
-               global_sign empty_named_context
+  let sign = 
+    List.fold_right
+      (fun (id,_,_ as d) s -> 
+	 if mem_named_context id current_sign then s else add_named_decl d s) 
+      global_sign empty_named_context
   in
-  let na = next_global_ident_away name
-             (ids_of_named_context global_sign) in
-  let concl = List.fold_left (fun t d -> mkNamedProd_or_LetIn d t)
-                (pf_concl gls) sign in
+  let na = next_global_ident_away name (ids_of_named_context global_sign) in
+  let concl = 
+    List.fold_left (fun t d -> mkNamedProd_or_LetIn d t) (pf_concl gls) sign 
+  in
+  if occur_existential concl then error "Cannot abstract with existentials";
   let lemme =
     start_proof na Declare.NeverDischarge current_sign concl;
     let _,(const,strength) =
@@ -1712,8 +1714,9 @@ let abstract_subproof name tac gls =
     let newenv = Global.env() in
     Declare.constr_of_reference Evd.empty newenv (ConstRef sp)
   in
-  exact_no_check (applist (lemme,
-		  List.map mkVar (List.rev (ids_of_named_context sign))))
+  exact_no_check 
+    (applist (lemme,
+	      List.map mkVar (List.rev (ids_of_named_context sign))))
     gls
 
 let tclABSTRACT name_op tac gls =