diff options
| author | Hugo Herbelin | 2020-08-19 14:57:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-25 22:27:31 +0200 |
| commit | 5d0c54e370ac20e9fbf249c3a7f1851a65e42acf (patch) | |
| tree | c443dae5ab8b2a207735fed5512f4c818b03a4e5 /vernac | |
| parent | 324e647cb9372dff2c12088524d8371fa3c1cd85 (diff) | |
Moving production_level_eq to extend.ml for separation of concerns.
Add a mli file and uniformize indentation on the way.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c9a03087e1..0bdcd53c92 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -665,13 +665,6 @@ let expand_list_rule s typ tkl x n p ll = aux (i+1) (main :: tks @ hds) ll in aux 0 [] ll -let production_level_eq lev1 lev2 = - match lev1, lev2 with - | NextLevel, NextLevel -> true - | NumLevel n1, NumLevel n2 -> Int.equal n1 n2 - | DefaultLevel, DefaultLevel -> true - | (NextLevel | NumLevel _| DefaultLevel), _ -> false - let is_constr_typ (s,lev) x etyps = match List.assoc x etyps with (* TODO: factorize these rules with the ones computing the effective |