From 7ffd9e720a7e615bd5a55c9e1a6674d3b69ba177 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 15 Apr 2004 15:53:21 +0000
Subject: Bug réaffichage EXT

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5678 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories7/Init/Logic_Type.v | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/theories7/Init/Logic_Type.v b/theories7/Init/Logic_Type.v
index 6fc7638076..b57484801b 100755
--- a/theories7/Init/Logic_Type.v
+++ b/theories7/Init/Logic_Type.v
@@ -72,8 +72,10 @@ Notation exT_intro := ex_intro (only parsing).
 Notation exT_ind  := ex_ind (only parsing).
 
 Notation ExT  := (ex ?).
-Notation "'EXT' x | p"      := (ex ? [x]p)    (at level 10, p at level 8).
-Notation "'EXT' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8).
+Notation "'EXT' x | p"      := (ex ? [x]p)
+  (at level 10, p at level 8, only parsing).
+Notation "'EXT' x : t | p"  := (ex ? [x:t]p)
+  (at level 10, p at level 8, only parsing).
 
 (*
 Inductive exT2 [A:Type;P,Q:A->Prop] : Prop
@@ -201,10 +203,10 @@ Notation identityT := identity (only parsing).
 Notation refl_identityT := refl_identity (only parsing).
 
 Notation "< A > x === y" := (!identityT A x y)
-   (A annot, at level 1, x at level 0, only parsing).
+   (A annot, at level 1, x at level 0, only parsing) : type_scope.
 
 Notation "x === y" := (identityT ? x y)
-  (at level 5, no associativity) : type_scope.
+  (at level 5, no associativity, only parsing) : type_scope.
 
 (*
 Hints Resolve refl_identityT : core v62.
-- 
cgit v1.2.3