diff options
| author | herbelin | 2003-09-11 19:56:40 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-11 19:56:40 +0000 |
| commit | 753f8765dec057f24238e1d039504f92e503386a (patch) | |
| tree | 77fc32b27596ffa40231ac9ad8f1dcf35cef53ed | |
| parent | 33d4c7f37cb0ee1cec0214d30336334959f3d84e (diff) | |
Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4353 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | theories/Init/Datatypes.v | 2 | ||||
| -rw-r--r-- | theories/Init/LogicSyntax.v | 6 | ||||
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 6 |
3 files changed, 9 insertions, 5 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index c0c999c4cf..cb2c272846 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -74,8 +74,10 @@ Section projections. Definition snd := [p:(prod A B)]Cases p of (pair x y) => y end. End projections. +V7only [ Notation Fst := (fst ? ?). Notation Snd := (snd ? ?). +]. Hints Resolve pair inl inr : core v62. diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index d3972eccd5..53940f2371 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -35,19 +35,19 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) (* Order is important to give printing priority to fully typed ALL and EX *) -Notation All := (all ?). +V7only [ 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 ? [x:t]p) (at level 10, p at level 8) V8only (at level 200). -Notation Ex := (ex ?). +V7only [ 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 ? [x:t]p) (at level 10, p at level 8) V8only (at level 200, x at level 80). -Notation Ex2 := (ex2 ?). +V7only [ 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). diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 627771fc41..eb9c7cc495 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -28,9 +28,11 @@ Notation "{ A } + { B }" := (sumbool A B). Notation "A + { B }" := (sumor A B). *) +V7only [ Notation ProjS1 := (projS1 ? ?). Notation ProjS2 := (projS2 ? ?). -Notation Except := (except ?). -Notation Error := (error ?). Notation Value := (value ?). +]. +Notation Except := (except ?). +Notation Error := (error ?). |