diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-11 19:24:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:04 +0100 |
| commit | 351e9acd3aa11a751129f5956fe991fc4d0bf0b8 (patch) | |
| tree | 55ce7af3e89df21649517cec521dc32225db18a5 /kernel/cClosure.ml | |
| parent | ead835b3e8c366800b8c95a28a89062abb62d807 (diff) | |
Introducing an intermediary type "constr_prod_entry_key" for grammar productions.
This type describes the grammar non-terminal. It typically contains
ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is
the type for metasyntax.ml and egramcoq.ml to communicate together.
The type constr_prod_entry_key with ETConstr, ETBinder, is now used
only in metasyntax.ml. This allows to get rid of some "assert false"
in uselessly matching over ETConstrList in metasyntax.ml and of some
"assert false" in uselessly matching over ETBinder in egramcoq.ml.
Also exporting less of extend.mli in API.
Diffstat (limited to 'kernel/cClosure.ml')
0 files changed, 0 insertions, 0 deletions