Généralisation de l'utilisation de Notation

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

9 files changed, 115 insertions, 249 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 9f72b6e174..26608a294d 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -59,7 +59,4 @@ Section projections.
    Definition snd := [p:(prod A B)]Cases p of (pair x y) => y end.
 End projections. 
 
-Syntactic Definition Fst := (fst ? ?).
-Syntactic Definition Snd := (snd ? ?).
-
 Hints Resolve pair inl inr : core v62.
diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
index a0543c7281..f1f7bba8a0 100644
--- a/theories/Init/DatatypesSyntax.v
+++ b/theories/Init/DatatypesSyntax.v
@@ -10,29 +10,16 @@
 
 Require Export Datatypes.
 
-(** Parsing of things in Datatypes.v *)
+(** Symbolic notations for things in [Datatypes.v] *)
 
-Grammar constr constr1 :=
-  pair_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "(" lconstr($c3) ","
-    lconstr($c4) ")" ] -> [ (pair $l1 $c2 $c3 $c4) ]
-| fst_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "("
-    lconstr($l) ")" ] -> [ (fst $l1 $c2 $l) ]
-| snd_expl [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "("
-    lconstr($l) ")" ] -> [ (snd $l1 $c2 $l) ]
+Infix LEFTA 4 "+" sum.
+Infix LEFTA 3 "*" prod.
+Notation "( x , y )" := (pair ? ? x y) (at level 0, x, y at level 10).
+Notation Fst := (fst ? ?).
+Notation Snd := (snd ? ?).
 
-with constr0 :=
-  pair [ "(" lconstr($lc1) "," lconstr($lc2) ")" ] ->
-         [ (pair ? ? $lc1 $lc2) ]
-.
+(** Parsing only of things in [Datatypes.v] *)
 
-Infix 4 "+" sum.
-Infix RIGHTA 3 "*" prod.
+Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing).
+Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing).
 
-(** Pretty-printing of things in Datatypes.v *)
-
-Syntax constr
-  level 1:
-    pair
-      [ (pair $_ $_ $t3 $t4) ] -> [ [<hov 0> "(" $t3:E ","[0 1] $t4:E ")" ] ]
-  | fst_imp [ (fst $_ $_ $t2) ] -> [ [<hov 0> "(Fst " $t2:E ")"] ]
-  | snd_imp [ (snd $_ $_ $t2) ] -> [ [<hov 0> "(Snd " $t2:E ")"] ].
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index a202038587..7636204ab9 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -220,9 +220,3 @@ Proof.
 Qed.
 
 Hints Immediate sym_eq sym_not_eq : core v62.
-
-
-
-Syntactic Definition Ex := ex | 1.
-Syntactic Definition Ex2 := ex2 | 1.
-Syntactic Definition All := all | 1.
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index fe796f9f27..6beae7d768 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -10,70 +10,50 @@
 
 Require Export Logic.
 
-(** Parsing of things in Logic.v *)
-
-Grammar constr constr1 :=
-  conj [ "<" lconstr($l1) "," lconstr($c2) ">" "{" constr($c3) ","
-        constr($c4) "}" ] -> [ (conj $l1 $c2 $c3 $c4) ]
-| proj1 [ "<" lconstr($l1) "," lconstr($c2) ">" "Fst" "{"
-        lconstr($l) "}" ] -> [ (proj1 $l1 $c2 $l) ]
-| proj2 [ "<" lconstr($l1) "," lconstr($c2) ">" "Snd" "{"
-        lconstr($l) "}" ] -> [ (proj2 $l1 $c2 $l) ]
-| all [ "<" lconstr($l1) ">" "All" "(" lconstr($l2) ")" ] ->
-      [ (all $l1 $l2) ]
-| eq_expl [ "<" lconstr($l1) ">" constr0($c1) "=" constr0($c2) ] ->
-          [ (eq $l1 $c1 $c2) ]
-| eq_impl [ constr0($c) "=" constr0($c2) ] -> [ (eq ? $c $c2) ]
-| IF [ "IF" constr($c1) "then" constr($c2) "else" constr($c3)] ->
-     [ (IF $c1 $c2 $c3) ]
-with constr10 :=
-  allexplicit [ "ALL" ident($x) ":" constr($t) "|" constr($p) ]
-                          -> [ (all $t [$x : $t]$p) ]
-| allimplicit [ "ALL" ident($x) "|" constr($p) ]
-                          -> [ (all ? [$x]$p) ]
-| exexplicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) ]
-                          -> [ (ex $t [$v : $t]$c1) ]
-| eximplicit [ "EX" ident($v) "|" constr($c1) ] 
-                          -> [ (ex ? [$v]$c1) ]
-| ex2explicit [ "EX" ident($v) ":" constr($t) "|" constr($c1) "&"
-           constr($c2) ] -> [ (ex2 $t [$v : $t]$c1 [$v : $t]$c2) ]
-| ex2implicit [ "EX" ident($v) "|" constr($c1) "&" 
-           constr($c2) ] -> [ (ex2 ? [$v]$c1 [$v]$c2) ].
+(** Symbolic notations for things in [Logic.v] *)
+
+Notation "< P , Q > { p , q }" := (conj P Q p q) (at level 1).
 
 Distfix RIGHTA 5 "~ _" not.
 
+Notation "x = y" := (eq ? x y) (at level 5).
+
 Infix RIGHTA 6 "/\\" and.
 
 Infix RIGHTA 7 "\\/" or.
 
 Infix RIGHTA 8 "<->" iff.
 
-(** Pretty-printing of things in Logic.v *)
+Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3)
+  (at level 1, c1, c2, c3 at level 8).
+
+(* Order is important to give printing priority to fully typed ALL and EX *)
+
+Notation All := (all ?).
+Notation "'ALL' x | p"     := (all ? [x]p)   (at level 10, p at level 8).
+Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8).
+
+Notation Ex  := (ex ?).
+Notation "'EX' x | p"      := (ex ? [x]p)    (at level 10, p at level 8).
+Notation "'EX' x : t | p"  := (ex t [x:t]p)  (at level 10, p at level 8).
+
+Notation Ex2 := (ex2 ?).
+Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
+  (at level 10, p, q at level 8).
+Notation "'EX' x : t | p & q"   := (ex2 t [x:t]p [x:t]q)
+  (at level 10, p, q at level 8).
+
+
+(** Parsing only of things in [Logic.v] *)
+
+Notation "< A > 'All' ( P )" := (all A P) (at level 1, only parsing).
+Notation "< A > x = y" := (eq A x y) (at level 1, x at level 0, only parsing).
+
+(** Pretty-printing only of things in [Logic.v] *)
 
 Syntax constr
   level 1:
     equal [ (eq $a  $t1  $t2) ] ->
 	 [ [<hov 0> (ANNOT $a) $t1:E [0 1]  "=" $t2:E ] ]
   | annotskip [ << (ANNOT $_) >> ] -> [ ]
-  | annotmeta [ << (ANNOT (META ($NUM $n))) >> ] -> [ "<" "?" $n ">" ]
-  | conj [ (conj $t1 $t2 $t3 $t4) ]
-      -> [ [<hov 1> [<hov 1> "<" $t1:L "," [0 0] $t2:L ">" ] [0 0]
-                    [<hov 1> "{" $t3:L "," [0 0] $t4:L "}"] ] ]
-  | IF [(IF $c1 then $c2 else $c3)] ->
-       [ [<hov 0> "IF " $c1:E [1 0]
-                  "then " $c2:E [1 0]
-                  "else " $c3:E ] ]
-  ;
-  level 10:
-    all_pred [ (all $_ $p) ] -> [ [<hov 4> "All " $p:L ] ]
-  | all_imp [ (all $_ [$x : $T]$t) ]
-       -> [ [<hov 3> "ALL " $x ":" $T:L " |" [1 0] $t:L ] ]
-
-  | ex_pred [ (ex $_ $p) ] -> [ [<hov 0> "Ex " $p:L ] ]
-  | ex [ (ex $_ [$x : $T]$P) ] 
-       -> [ [<hov 2> "EX " $x ":" $T:L " |" [1 0] $P:L ] ]
-
-  | ex2_pred [ (ex2 $_ $p1 $p2) ]
-       -> [ [<hov 3> "Ex2 " $p1:L [1 0] $p2:L ] ]
-  | ex2 [ (ex2 $_ [$x : $T]$P1 [$x : $T]$P2) ] 
-       -> [ [<hov 2> "EX " $x ":" $T:L " |" [1 2] $P1:L [1 0] "& " $P2:L] ].
+  | annotmeta [ << (ANNOT (META ($NUM $n))) >> ] -> [ "<" "?" $n ">" ].
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 80cd878b10..e4982c1f64 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -198,10 +198,6 @@ Definition prodT_curry : (A,B,C:Type)(A->B->C)->(prodT A B)->C :=
 
 Hints Immediate sym_idT sym_not_idT : core v62.
 
-Syntactic Definition AllT := allT | 1.
-Syntactic Definition ExT := exT | 1.
-Syntactic Definition ExT2 := exT2 | 1.
-
 Implicits fstT [1 2].
 Implicits sndT [1 2].
 Implicits pairT [1 2].
diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v
index 96d3b74b83..25b67ad938 100644
--- a/theories/Init/Logic_TypeSyntax.v
+++ b/theories/Init/Logic_TypeSyntax.v
@@ -10,49 +10,38 @@
 
 Require Logic_Type.
 
-(** Parsing of things in [Logic_type.v] *)
-
-Grammar constr constr1 :=
-  eqT_expl [ "<" lconstr($l1) ">" constr0($c1) "==" constr0($c2) ] ->
-          [ (eqT $l1 $c1 $c2) ]
-| eqT_impl [ constr0($c) "==" constr0($c2) ] -> [ (eqT ? $c $c2) ]
-| idT_expl [ "<" lconstr($l1) ">" constr0($c1) "===" constr0($c2) ] ->
-          [ (identityT $l1 $c1 $c2) ]
-| idT_impl [ constr0($c) "===" constr0($c2) ] -> [ (identityT ? $c $c2) ]
-
-with constr10 :=
-  allTexplicit [ "ALLT" ident($v) ":" constr($t) "|" constr($c1) ]
-                          -> [ (allT $t [$v : $t]$c1) ]
-| allTimplicit [ "ALLT" ident($v) "|" constr($c1) ] 
-                          -> [ (allT ? [$v]$c1) ]
-| exTexplicit [ "EXT" ident($v) ":" constr($t) "|" constr($c1) ]
-                          -> [ (exT $t [$v : $t]$c1) ]
-| exTimplicit [ "EXT" ident($v) "|" constr($c1) ] 
-                          -> [ (exT ? [$v]$c1) ]
-| exT2explicit [ "EXT" ident($v) ":" constr($t) "|" constr($c1) "&"
-           constr($c2) ] -> [ (exT2 $t [$v : $t]$c1 [$v : $t]$c2) ]
-| exT2implicit [ "EXT" ident($v) "|" constr($c1) "&" 
-           constr($c2) ] -> [ (exT2 ? [$v]$c1 [$v]$c2) ].
-
-(** Pretty-printing of things in [Logic_type.v] *)
+(** Symbolic notations for things in [Logic_type.v] *)
 
-Syntax constr
-  level 10:
-    allT_pred [ (allT $_ $p) ] -> [ [<hov 0> "AllT " $p:L ] ]
-  | allT [ (allT $T [$x : $T]$p) ]
-       -> [ [<hov 3> "ALLT " $x ":" $T:L " |" [1 0] $p:L ] ]
+Notation "x == y"  := (eqT ? x y)       (at level 5).
+Notation "x === y" := (identityT ? x y) (at level 5).
+
+(* Order is important to give printing priority to fully typed ALL and EX *)
+
+Notation AllT := (allT ?).
+Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8).
+Notation "'ALLT' x | p"     := (allT ? [x]p)   (at level 10, p at level 8).
+
+Notation ExT  := (exT ?).
+Notation "'EXT' x : t | p"  := (exT t [x:t]p)  (at level 10, p at level 8).
+Notation "'EXT' x | p"      := (exT ? [x]p)    (at level 10, p at level 8).
 
-  | exT_pred [ (exT $_ $p) ] -> [ [<hov 4> "ExT " $p:L ] ]
-  | exT [ (exT $t1 [$x : $T]$p) ] 
-       -> [ [<hov 4> "EXT " $x ":" $T:L " |" [1 0] $p:L ] ]
+Notation ExT2 := (exT2 ?).
+Notation "'EXT' x : t | p & q" := (exT2 t [x:t]p [x:t]q)
+  (at level 10, p, q at level 8).
+Notation "'EXT' x | p & q"     := (exT2 ? [x]p [x]q)
+  (at level 10, p, q at level 8).
 
-  | exT2_pred [ (exT2 $_ $p1 $p2) ]
-       -> [ [<hov 4> "ExT2 " $p1:L [1 0] $p2:L ] ]
-  | exT2 [ (exT2 $T [$x : $T]$P1 [$x : $T]$P2) ] 
-       -> [ [<hov 2> "EXT " $x ":" $T:L " |" [1 2] $P1:L [1 0] "& " $P2:L] ]
-  ;
+(** Parsing only of things in [Logic_type.v] *)
 
+Notation "< A > x == y"  := (eqT A x y)
+   (at level 1, x at level 0, only parsing).
+
+Notation "< A > x === y" := (identityT A x y)
+   (at level 1, x at level 0, only parsing).
+
+(** Pretty-printing only of things in [Logic_type.v] *)
+
+Syntax constr
   level 1:
-    eqT [ (eqT $a $c1 $c2) ] -> [ [<hov 1> (ANNOT $a) $c1:E [0 0] "==" $c2:E ] ]
-  | identityT [ (identityT $_ $c1 $c2) ]
-       -> [ [<hov 1> $c1:E [0 0] "===" $c2:E ] ].
+   eqT [ (eqT $a $c1 $c2) ] -> [ [<hov 1> (ANNOT $a) $c1:E [0 0] "==" $c2:E ] ]
+.
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index cbf5c2d207..adb917b765 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -16,7 +16,7 @@ Syntax constr
   | O [ O ]      -> ["(0)"].
 
 (* Outside the module to be able to parse the grammar for 0,1,2... !! *)
-Delimiters "'N:" nat_scope "'". (* "[N", "[N:", "]]" are conflicting *)
+Delimits Scope nat_scope with N.
 
 (* For parsing/printing based on scopes *)
 Module nat_scope.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index f9010f4dd3..daf7e5d85b 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -82,9 +82,6 @@ Section Projections.
 
 End Projections.
 
-Syntactic Definition ProjS1 := (projS1 ? ?).
-Syntactic Definition ProjS2 := (projS2 ? ?).
-
 
 Section Extended_booleans.
 
@@ -150,13 +147,8 @@ Definition Exc := option.
 Definition value := Some.
 Definition error := None.
 
-Syntactic Definition Error := (error ?).
-Syntactic Definition Value := (value ?).
-
 Definition except := False_rec. (* for compatibility with previous versions *)
 
-Syntactic Definition Except := (except ?).
-
 Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C.
 Proof.
   Intros A C h1 h2.
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 8d32dcfc86..a617373c82 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -8,118 +8,49 @@
 
 (*i $Id$ i*)
 
-Require Datatypes.
-Require LogicSyntax.
+Require DatatypesSyntax.
 Require Specif.
 
-(** Parsing of things in Specif.v *)
-
-(* To accept {x:A|P}*B without parentheses *)
-Grammar constr constr3 :=
-  sigprod [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}"
-            "*" constr3($c) ]
-       -> [ (prod (sig $c1 [$lc : $c1]$c2) $c) ]
-
-| sig2prod [ "{" lconstr($lc) ":" lconstr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ]
-       -> [ (prod (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ]
-
-| sigSprod [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}"
-         "*" constr3($c)]
-       -> [ (prod (sigS $c1 [$lc : $c1]$c2) $c) ]
-
-| sigS2prod [ "{" lconstr($lc) ":" lconstr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" "*" constr3($c) ]
-       -> [ (prod (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) $c) ].
-
-(* To factor with {A}+{B} *)
-Grammar constr constr3 :=
-  sig [ "{" lconstr($lc) ":" lconstr($c1) "|" lconstr($c2) "}" ]
-       -> [ (sig $c1 [$lc : $c1]$c2) ]
-
-| sig2 [ "{" lconstr($lc) ":" lconstr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [ (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ]
-
-| sigS [ "{" lconstr($lc) ":" lconstr($c1) "&" lconstr($c2) "}" ]
-       -> [ (sigS $c1 [$lc : $c1]$c2) ]
-
-| sigS2 [ "{" lconstr($lc) ":" lconstr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [ (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3) ].
-
-Notation 3 "{ x } + { y }" (sumbool x y).
-Notation LEFTA 4 " x + { y }" (sumor x y).
-
-Grammar constr lassoc_constr4 :=
-  sumsig [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1) "|" lconstr($c2) "}" ] ->
-    [ (sum $c (sig $c1 [$lc : $c1]$c2)) ]
-
-| sumsig2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1)
-           "|" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [ (sum $c (sig2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
-
-| sumsigS [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1) "&" lconstr($c2) "}" ]
-       -> [ (sum $c (sigS $c1 [$lc : $c1]$c2)) ]
-
-| sumsigS2 [ lassoc_constr4($c) "+" "{" lconstr($lc) ":" constr($c1)
-             "&" lconstr($c2) "&" lconstr($c3) "}" ]
-       -> [ (sum $c (sigS2 $c1 [$lc : $c1]$c2 [$lc : $c1]$c3)) ]
-.
-
-
-(** Pretty-printing of things in Specif.v *)
-
-Syntax constr
-  level 1:
-(** Pretty-printing of [sig] *)
-  | sig_nb [ (sig $c1 [_:$1]$c2) ]
-      -> [ [<hov 0> "{_:" $c1:E " |" [1 3] $c2:E "}" ] ]
-  | sigma_b [ (sig $c1 [$id:$1]$c2) ]
-      -> [ [<hov 0> "{" $id ":" $c1:E " |" [1 3] $c2:E "}" ] ]
-
-(** Pretty-printing of [sig2] *)
-  | sig2_b_b
-      [ (sig2 $c1 [$id:$c1]$c2 [$id:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sig2_nb_b
-      [ (sig2 $c1 [_:$c1]$c2 [$id:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sig2_b_nb
-      [ (sig2 $c1 [$id:$c1]$c2 [_:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id":"$c1:E"|" [1 3]$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sig2_nb_nb
-      [ (sig2 $c1 [_:$c1]$c2 [_:$c1]$c3) ]
-       -> [ [<hov 0> "{_:"$c1:E "|" [1 3] $c2:E [1 3]"& " $c3:E "}" ] ]
-
-(** Pretty-printing of [sigS] *)
-  | sigS_nb [ (sigS $c1 [_:$c1]$c2) ]
-       -> [ [<hov 0> "{_:" $c1:E [1 3]"& " $c2:E  "}" ] ]
-  | sigS_b [ (sigS $c1 [$id:$c1]$c2) ]
-       -> [ [<hov 0> "{" $id  ":" $c1:E [1 3] "& " $c2:E "}" ] ]
-
-(** Pretty-printing of [sigS2] *)
-  | sigS2_b_b
-      [ (sigS2 $c1 [$id:$c1]$c2 [$id:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sigS2_nb_b
-      [ (sigS2 $c1 [_:$c1]$c2 [$id:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sigS2_b_nb
-      [ (sigS2 $c1 [$id:$c1]$c2 [_:$c1]$c3) ]
-       -> [ [<hov 0> "{"$id ":" $c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
-  | sigS2_nb_nb
-      [ (sigS2 $c1 [_:$c1]$c2 [_:$c1]$c3) ]
-       -> [ [<hov 0> "{_:"$c1:E [1 3]"& "$c2:E [1 3]"& "$c3:E "}" ] ]
-
-(** Pretty-printing of [projS1] and [projS2] *)
-  | projS1_imp [ (projS1 ? ? $a) ] -> ["(ProjS1 " $a:E ")"]  
-  | projS2_imp [ (projS2 ? ? $a) ] -> ["(ProjS2 " $a:E ")"]
-
-(** Pretty-printing of [except] *)
-  | Except_imp [ (except $1 $t2) ] -> [ [<hov 0> "Except " $t2 ] ]
-
-(** Pretty-printing of [error] and [value] *)
-  | Error_imp [ (error $t1) ]     -> [ [<hov 0> "Error" ] ]
-  | Value_imp [ (value $t1 $t2) ] -> [ [<hov 0> "(Value " $t2 ")" ] ].
+(** Symbolic notations for things in [Specif.v] *)
+
+(* At level 1 to factor with {x:A|P} etc *)
+Notation "{ A } + { B }" := (sumbool A B)
+  (at level 1, A at level 10, B at level 10).
+
+Notation "A + { B }" := (sumor A B)
+  (at level 4, B at level 10, left associativity).
+
+Notation ProjS1 := (projS1 ?).
+Notation ProjS2 := (projS2 ?).
+Notation Error  := (error ?).
+Notation Value  := (value ?).
+Notation Except := (except ?).
+
+Notation "{ x : A  |  P }"       := (sig A [x:A]P)
+  (at level 1, x at level 10).
+
+Notation "{ x : A  |  P  &  Q }" := (sig2 A [x:A]P [x:A]Q)
+  (at level 1, x at level 10).
+
+Notation "{ x : A  &  P }"       := (sigS A [x:A]P)
+  (at level 1, x at level 10).
+
+Notation "{ x : A  &  P  &  Q }" := (sigS2 A [x:A]P [x:A]Q)
+  (at level 1, x at level 10).
+
+(** Extra factorization of parsing rules *)
+
+(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *)
+
+Notation "B + { x : A | P }"     := B + ({x:A | P})
+  (at level 4, x at level 10, left associativity, only parsing).
+
+Notation "B + { x : A | P & Q }" := B + ({x:A | P & Q})
+  (at level 4, x at level 10, left associativity, only parsing).
+
+Notation "B + { x : A & P }"     := B + ({x:A & P})
+  (at level 4, x at level 10, left associativity, only parsing).
+
+Notation "B + { x : A & P & Q }" := B + ({x:A & P & Q})
+  (at level 4, x at level 10, left associativity, only parsing).