Suppression d'une occurrence superflue d'argument de type dans Notation sachant que les 2 occurrences ne sont pas forcement dans le meme scope

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

2 files changed, 7 insertions, 6 deletions

diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index a16583dd40..d3972eccd5 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -38,20 +38,20 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3)
 Notation All := (all ?).
 Notation "'ALL' x | p"     := (all ? [x]p)   (at level 10, p at level 8)
   V8only (at level 200, p at level 200).
-Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8)
+Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8)
   V8only (at level 200).
 
 Notation Ex  := (ex ?).
 Notation "'EX' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
-Notation "'EX' x : t | p"  := (ex t [x:t]p)  (at level 10, p at level 8)
+Notation "'EX' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
 
 Notation Ex2 := (ex2 ?).
 Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 8)
   V8only "'EX2' x | p & q" (at level 200, x at level 80).
-Notation "'EX' x : t | p & q"   := (ex2 t [x:t]p [x:t]q)
+Notation "'EX' x : t | p & q"   := (ex2 ? [x:t]p [x:t]q)
   (at level 10, p, q at level 8)
   V8only "'EX2' x : t | p & q" (at level 200, x at level 80).
 
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 6eb768ef0a..21dd4ccec6 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -8,6 +8,7 @@
 
 (*i $Id$ i*)
 
+Require Notations.
 Require Logic_Type.
 
 (** Symbolic notations for things in [Logic_type.v] *)
@@ -21,20 +22,20 @@ Notation "x === y" := (identityT ? x y) (at level 5, no associativity).
 Notation AllT := (all ?).
 Notation "'ALLT' x | p"     := (all ? [x]p)   (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
-Notation "'ALLT' x : t | p" := (all t [x:t]p) (at level 10, p at level 8)
+Notation "'ALLT' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
 
 Notation ExT  := (ex ?).
 Notation "'EXT' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
-Notation "'EXT' x : t | p"  := (ex t [x:t]p)  (at level 10, p at level 8)
+Notation "'EXT' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8)
   V8only (at level 200, x at level 80).
 
 Notation ExT2 := (ex2 ?).
 Notation "'EXT' x | p & q"     := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 8)
   V8only "'EXT2' x | p & q" (at level 200, x at level 80).
-Notation "'EXT' x : t | p & q" := (ex2 t [x:t]p [x:t]q)
+Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q)
   (at level 10, p, q at level 8)
   V8only "'EXT2' x : t | p & q" (at level 200, x at level 80).
 ].