diff options
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/egramcoq.ml | 8 | ||||
-rw-r--r-- | parsing/egramcoq.mli | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ec422c58d..870137ca1 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -443,7 +443,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function CAst.make ~loc @@ CPatNotation (notation, env, []) let extend_constr state forpat ng = - let n = ng.notgram_level in + let n,_,_ = ng.notgram_level in let assoc = ng.notgram_assoc in let (entry, level) = interp_constr_entry_key forpat n in let fold (accu, state) pt = @@ -464,7 +464,7 @@ let extend_constr state forpat ng = let constr_levels = GramState.field () -let extend_constr_notation (_, ng) state = +let extend_constr_notation ng state = let levels = match GramState.get state constr_levels with | None -> default_constr_levels | Some lev -> lev @@ -476,7 +476,7 @@ let extend_constr_notation (_, ng) state = let state = GramState.set state constr_levels levels in (r @ r', state) -let constr_grammar : (Notation.level * notation_grammar) grammar_command = +let constr_grammar : one_notation_grammar grammar_command = create_grammar_command "Notation" extend_constr_notation -let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) +let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 248de3348..8e0469275 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -13,5 +13,5 @@ (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit +val extend_constr_grammar : Notation_term.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) |