From dce9fe9bd4cab3e560f41a8d7cbf447b27665e1f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 13 Sep 2009 13:24:21 +0000
Subject: - 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
---
 parsing/g_vernac.ml4 | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 272737cc68..2a5dc64bcc 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 | -> [] ]
-- 
cgit v1.2.3