diff options
| author | herbelin | 2003-09-23 11:23:14 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-23 11:23:14 +0000 |
| commit | 58b3bc4b3151bc5f8b81fbc7a1943f99b081f80e (patch) | |
| tree | 32269fe01cb1488a1d6ab4e0a9d0ec64efb3deee /theories/Init/SpecifSyntax.v | |
| parent | 4d7184fe2f570f123eef72c88d6d3f082617bd2a (diff) | |
Fusion des fichiers de syntaxe de Init avec les fichiers de définition; TypeSyntax inutile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4461 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/SpecifSyntax.v')
| -rw-r--r-- | theories/Init/SpecifSyntax.v | 38 |
1 files changed, 0 insertions, 38 deletions
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v deleted file mode 100644 index eb9c7cc495..0000000000 --- a/theories/Init/SpecifSyntax.v +++ /dev/null @@ -1,38 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -Require Notations. -Require Datatypes. -Require Specif. - -(** Extra factorization of parsing rules *) - -(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) - -Notation "B + { x : A | P }" := B + (sig A [x:A]P) (only parsing). -Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) (only parsing). -Notation "B + { x : A & P }" := B + (sigS A [x:A]P) (only parsing). -Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) (only parsing). - -(** Symbolic notations for definitions in [Specif.v] *) - -(* -Notation "{ A } + { B }" := (sumbool A B). -Notation "A + { B }" := (sumor A B). -*) - -V7only [ -Notation ProjS1 := (projS1 ? ?). -Notation ProjS2 := (projS2 ? ?). -Notation Value := (value ?). -]. - -Notation Except := (except ?). -Notation Error := (error ?). |