Clarification de l'ordre d'interprétation des variables dans ltac. En

particulier, TacCall(_,f,[]) est utilisé pour une référence à une
variable ltac ou une tactique et Reference(f) est utilisé pour une
référence à une variable ltac ou un constr (en passant,
standardisation de l'utilisation de constr: ou ltac: à setoid_ring).



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

1 files changed, 12 insertions, 1 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 9dd7b273d..757cf6a4e 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -173,7 +173,7 @@ Abort.
    empty args *)
 
 Goal True.
-match None with @None => exact I end.
+match constr:@None with @None => exact I end.
 Abort.
 
 (* Check second-order pattern unification *)
@@ -209,3 +209,14 @@ Goal True -> True -> True.
 is.
 exact I.
 Abort.
+
+(* Interférence entre espaces des noms *)
+
+Ltac O := intro.
+Ltac Z1 t := set (x:=t).
+Ltac Z2 t := t.
+Goal True -> True.
+Z1 O.
+Z2 ltac:O.
+exact I.
+Qed.