Backtrack sur la réparation de Abstract qui casse autre chose; le problème en présence de variables de section est plus subtil et sa résolution est reportée

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

1 files changed, 13 insertions, 4 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 15c161742f..285e3fa562 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1873,12 +1873,21 @@ let intros_transitivity  n  = tclTHEN intros (transitivity n)
 
 let abstract_subproof name tac gls = 
   let env = Global.env() in
-  let sign = pf_hyps gls in
-  let na = next_global_ident_away false name (ids_of_named_context sign) in
+  let current_sign = Global.named_context()
+  and global_sign = pf_hyps gls in
+  let sign,secsign = 
+    List.fold_right
+      (fun (id,_,_ as d) (s1,s2) -> 
+	 if mem_named_context id current_sign then (s1,add_named_decl d s2)
+	 else (add_named_decl d s1,s2)) 
+      global_sign (empty_named_context,empty_named_context) 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";
+  if occur_existential concl then
+    if !Options.v7 then error "Abstract cannot handle existentials"
+    else error "\"abstract\" cannot handle existentials";
   let lemme =
-    start_proof na (IsGlobal (Proof Lemma)) [] concl (fun _ _ -> ());
+    start_proof na (IsGlobal (Proof Lemma)) secsign concl (fun _ _ -> ());
     let _,(const,kind,_) =
       try
 	by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac));