diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:31:38 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:31:38 +0200 |
| commit | 041c6c02c2c71b442cf4765918f5c6685c4d92f0 (patch) | |
| tree | babe6b0f86c072459fb1d3b2c412c62e11ea5dfd /parsing | |
| parent | 8c097e35835c4a31a24c043c1bc36ff9d356a87c (diff) | |
| parent | b71e68fb78ccde52f1aaa63ef26f0135b92e9be5 (diff) | |
Merge PR #1037: Parse directly to Sorts.family when appropriate.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 10 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
4 files changed, 15 insertions, 6 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index f637e9746..7d0728458 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -123,8 +123,8 @@ let name_colon = let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr universe_level sort global - constr_pattern lconstr_pattern Constr.ident + GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family + global constr_pattern lconstr_pattern Constr.ident closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; Constr.ident: @@ -149,6 +149,12 @@ GEXTEND Gram | "Type"; "@{"; u = universe; "}" -> GType u ] ] ; + sort_family: + [ [ "Set" -> Sorts.InSet + | "Prop" -> Sorts.InProp + | "Type" -> Sorts.InType + ] ] + ; universe: [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids | id = name -> [id] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b9a162bec..5b044d2f0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -340,13 +340,13 @@ GEXTEND Gram ; scheme_kind: [ [ IDENT "Induction"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) + IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s) | IDENT "Minimality"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) + IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s) | IDENT "Elimination"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> CaseScheme(true,ind,s) + IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s) | IDENT "Case"; "for"; ind = smart_global; - IDENT "Sort"; s = sort-> CaseScheme(false,ind,s) + IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s) | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] ; (* Various Binders *) 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); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 445818e13..897e42c30 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -225,6 +225,7 @@ module Constr : val global : reference Gram.entry val universe_level : glob_level Gram.entry val sort : glob_sort Gram.entry + val sort_family : Sorts.family Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry val lconstr_pattern : constr_expr Gram.entry |