diff options
| author | Arnaud Spiwack | 2014-09-02 18:02:26 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:54 +0200 |
| commit | ac2fdfb222083faa9c3893194e020bed38555ddb (patch) | |
| tree | df170292bb8d960469a3653d8f7481b42599fbf9 /parsing | |
| parent | c907f31fd8f4b12bf2d7df2078603dbe804475a2 (diff) | |
Add a [Variant] declaration which allows to write non-recursive variant types.
Just like the [Record] keyword allows only non-recursive records.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 013381382e..3437256ed2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -269,7 +269,8 @@ GEXTEND Gram ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) - | "CoInductive" -> (CoInductive,CoFinite) ] ] + | "CoInductive" -> (CoInductive,CoFinite) + | "Variant" -> (Variant,BiFinite) ] ] ; infer_token: [ [ IDENT "Infer" -> true | -> false ] ] |