From 4fdedbe7d0a527044a56a769aff272b1f07b2ac5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 15 Mar 2004 13:55:40 +0000
Subject: Nouvelle reparation pour Abstract en presence de variables de
 contexte: on considere une var de but comme var de contexte si elle a meme
 nom, meme type, et, le cas echeant meme corps

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5487 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 285e3fa562..695bb3bc7a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1871,6 +1871,11 @@ let intros_transitivity  n  = tclTHEN intros (transitivity n)
    the current goal, abstracted with respect to the local signature, 
    is solved by tac *)
 
+let interpretable_as_section_decl d1 d2 = match d1,d2 with
+  | (_,Some _,_), (_,None,_) -> false
+  | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2
+  | (_,None,t1), (_,_,t2) -> eq_constr t1 t2
+
 let abstract_subproof name tac gls = 
   let env = Global.env() in
   let current_sign = Global.named_context()
@@ -1878,7 +1883,9 @@ 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 then (s1,add_named_decl d s2)
+	 if mem_named_context id current_sign &
+           interpretable_as_section_decl (Sign.lookup_named id current_sign) d
+         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
-- 
cgit v1.2.3