diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-08 14:58:28 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-08 18:42:37 +0200 |
| commit | b71e68fb78ccde52f1aaa63ef26f0135b92e9be5 (patch) | |
| tree | fd07ca12f3aa602a082cc960a82f031ea72fa7c3 /parsing/pcoq.ml | |
| parent | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (diff) | |
Parse directly to Sorts.family when appropriate.
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 81f02bf95..0d24599ea 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -471,6 +471,7 @@ module Constr = let global = make_gen_entry uconstr "global" let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" + let sort_family = make_gen_entry uconstr "sort_family" let pattern = Gram.entry_create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" let lconstr_pattern = gec_constr "lconstr_pattern" @@ -631,6 +632,7 @@ let () = Grammar.register0 wit_ident (Prim.ident); Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); + Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); Grammar.register0 wit_red_expr (Vernac_.red_expr); () |