diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /parsing | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index b3ae24e941..6f73a3e4ed 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -31,7 +31,7 @@ let ldots_var = Id.of_string ".." let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "Prop"; "Set"; "Type"; ".("; "_"; ".."; + "SProp"; "Prop"; "Set"; "Type"; ".("; "_"; ".."; "`{"; "`("; "{|"; "|}" ] let _ = List.iter CLexer.add_keyword constr_kw @@ -153,6 +153,7 @@ GRAMMAR EXTEND Gram sort: [ [ "Set" -> { GSet } | "Prop" -> { GProp } + | "SProp" -> { GSProp } | "Type" -> { GType [] } | "Type"; "@{"; u = universe; "}" -> { GType u } ] ] @@ -160,6 +161,7 @@ GRAMMAR EXTEND Gram sort_family: [ [ "Set" -> { Sorts.InSet } | "Prop" -> { Sorts.InProp } + | "SProp" -> { Sorts.InSProp } | "Type" -> { Sorts.InType } ] ] ; @@ -323,6 +325,7 @@ GRAMMAR EXTEND Gram ; universe_level: [ [ "Set" -> { GSet } + (* no parsing SProp as a level *) | "Prop" -> { GProp } | "Type" -> { GType UUnknown } | "_" -> { GType UAnonymous } |