diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:41:36 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:41:36 +0200 |
| commit | 9326b0466cc04175436dc57cf0283c151b587e54 (patch) | |
| tree | efa25b429b80403105431c8ea21bae475dffea8e /parsing | |
| parent | 57af4b4112dd0bc54badf0faebb373ef70ea2c1a (diff) | |
| parent | 414a30432119bcc878793b33144f671403132f7a (diff) | |
Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructuration
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. *) |