diff options
| author | herbelin | 2004-02-17 09:23:50 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-17 09:23:50 +0000 |
| commit | 6d42453dea17a8bd35530bf793344570ff9fc055 (patch) | |
| tree | d7ab7bd9934c0c48f80a3c3d88a1de8e20636f12 /parsing | |
| parent | 4f6a3a7968bfe6f6551f0f5902d3d76a7b69cd25 (diff) | |
Ajout de lconstr, constr et binder_constr dans Print Grammar constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5355 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |