diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-27 09:25:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-27 09:25:49 +0000 |
| commit | f6c57e62abb2b208bafbcc12c4b8afd742b82474 (patch) | |
| tree | 916e533b12c79e603c2a66e9cd7fc9f680c1c1cf /parsing | |
| parent | 67078a0f6e58590d5a5fd835439bbf7d29bcc880 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egrammar.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index f54b31484..e8292bf05 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 |