diff options
| author | herbelin | 2004-03-15 13:55:40 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-15 13:55:40 +0000 |
| commit | 4fdedbe7d0a527044a56a769aff272b1f07b2ac5 (patch) | |
| tree | 0788d06abfb98af230dba05a77baccac1b96a6df | |
| parent | d1c57fb01e6e4453520a46710455c0612656925f (diff) | |
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
| -rw-r--r-- | tactics/tactics.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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 |