From b483429713477413e7432856e862aa69ca644724 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 30 Sep 2003 15:12:43 +0000
Subject: Les notations hors scope s'empilent maintenant comme des scopes ne
 contenant qu'une notation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4503 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/extend.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'parsing/extend.ml')

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 6a557f368..1a9bdec91 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -91,6 +91,7 @@ type syntax_modifier =
   | SetAssoc of Gramext.g_assoc
   | SetEntryType of string * simple_constr_production_entry
   | SetOnlyParsing
+  | SetFormat of string
 
 type nonterm =
   | NtShort of string
@@ -289,7 +290,7 @@ type 'pat unparsing_hunk =
   | UNP_TBRK of int * int
   | UNP_TAB
   | UNP_FNL
-  | UNP_SYMBOLIC of string * string * 'pat unparsing_hunk
+  | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk
 
 let rec subst_hunk subst_pat subst hunk = match hunk with
   | PH (pat,so,pr) ->
-- 
cgit v1.2.3