aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-13 13:24:21 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-13 13:24:21 +0000
commitdce9fe9bd4cab3e560f41a8d7cbf447b27665e1f (patch)
treeb41dc8ddb21f8dd9511942010864b75b426e6cbc /parsing
parent01258eb971a3ed22e65a0f9427a870be82f5ceb7 (diff)
- Inductive types in the "using" option of auto/eauto/firstorder are
interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_vernac.ml44
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 272737cc6..2a5dc64bc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -833,6 +833,10 @@ GEXTEND Gram
pil = LIST1 production_item; ":="; t = Tactic.tactic
-> VernacTacticNotation (n,pil,t)
+ | IDENT "Reserved"; IDENT "Infix"; s = ne_string;
+ l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
+ VernacSyntaxExtension (use_locality (),("_ '"^s^"' _",l))
+
| IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
s = ne_string;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]