From f6c57e62abb2b208bafbcc12c4b8afd742b82474 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 27 Nov 2004 09:25:49 +0000
Subject: Indépendance vis à vis de Symbols (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6361 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/egrammar.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index f54b31484d..e8292bf051 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -14,6 +14,7 @@ open Topconstr
 open Ast
 open Coqast
 open Vernacexpr
+open Ppextend
 open Extend
 open Rawterm
 open Mod_subst
@@ -23,7 +24,7 @@ type notation_grammar =
     int * Gramext.g_assoc option * notation * prod_item list * int list option
 
 type all_grammar_command =
-  | Notation of Symbols.level * notation_grammar
+  | Notation of (precedence * tolerability list) * notation_grammar
   | Grammar of grammar_command
   | TacticGrammar of
       (string * (string * grammar_production list) * 
@@ -55,4 +56,5 @@ val subst_all_grammar_command :
 val interp_entry_name : string -> string -> 
   entry_type * Token.t Gramext.g_symbol
 
-val recover_notation_grammar :  notation -> Symbols.level -> notation_grammar
+val recover_notation_grammar :
+  notation -> (precedence * tolerability list) -> notation_grammar
-- 
cgit v1.2.3