diff options
| author | Hugo Herbelin | 2017-08-11 19:24:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:04 +0100 |
| commit | 351e9acd3aa11a751129f5956fe991fc4d0bf0b8 (patch) | |
| tree | 55ce7af3e89df21649517cec521dc32225db18a5 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 950246c531..a7e73c91f4 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -102,7 +102,6 @@ open Decl_kinds | ETBigint -> str "bigint" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" - | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" let pr_comment pr_c = function | CommentConstr c -> pr_c c |