diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-11 11:28:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-11 15:16:10 +0200 |
| commit | df2d71323081f8a395881ffc0e1793e429abc3bb (patch) | |
| tree | 66e77810a4df69233c577c20732c06cdccf1d9db /parsing/egramcoq.ml | |
| parent | 17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c (diff) | |
Turning the grammar extend command API into a state-passing one.
Diffstat (limited to 'parsing/egramcoq.ml')
| -rw-r--r-- | parsing/egramcoq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 9cfd534b0..72cb14bad 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -343,12 +343,12 @@ let extend_constr forpat ng = in List.fold_left fold 0 ng.notgram_prods -let extend_constr_notation (_, ng) = +let extend_constr_notation (_, ng) state = (* Add the notation in constr *) let nb = extend_constr ForConstr ng in (* Add the notation in cases_pattern *) let nb' = extend_constr ForPattern ng in - nb + nb' + (nb + nb', state) let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation |