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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index dce073becb..514017d454 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -652,7 +652,7 @@ let rec pr_vernac = function let (_,_,_,k,_),_ = List.hd l in match k with Record -> "Record" | Structure -> "Structure" | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" in + | Class _ -> "Class" | Variant -> "Variant" in hov 1 (pr_oneind key (List.hd l)) ++ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) |