diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 21:42:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 21:42:58 +0000 |
| commit | 90e5407fcfc59dce5ea592aeae6195183a2b4ad2 (patch) | |
| tree | a30c7aebc8d840b87d702b972fbbff16714e4b6d /parsing/g_vernac.ml4 | |
| parent | 0b6924f05ef6beb775345f3fb2ad21a009ab3baa (diff) | |
Ajout d'abbréviations/notations paramétriques
Example: "Notation reflexive R := (forall x, R x x)."
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index df29d5096..a693ebdb5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -794,9 +794,10 @@ GEXTEND Gram modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (local,(op,modl),p,sc) - | IDENT "Notation"; local = locality; id = ident; ":="; c = constr; + | IDENT "Notation"; local = locality; id = ident; idl = LIST0 ident; + ":="; c = constr; b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> - VernacSyntacticDefinition (id,c,local,b) + VernacSyntacticDefinition (id,(idl,c),local,b) | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> |