diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index e0b60e6243..296c66b07a 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -343,6 +343,7 @@ module Constr = let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr let lconstr = gec_constr "lconstr" + let binder_constr = create_constr_entry uconstr "binder_constr" let ident = make_gen_entry uconstr rawwit_ident "ident" let global = make_gen_entry uconstr rawwit_ref "global" let sort = make_gen_entry uconstr rawwit_sort "sort" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 1ad4bbfd8f..c245f9fd5e 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -132,6 +132,7 @@ module Constr : val constr : constr_expr Gram.Entry.e val constr_eoi : constr_expr Gram.Entry.e val lconstr : constr_expr Gram.Entry.e + val binder_constr : constr_expr Gram.Entry.e val operconstr : constr_expr Gram.Entry.e val ident : identifier Gram.Entry.e val global : reference Gram.Entry.e |