From a93dbac35ed828286b0af9e5c6597081ed24a553 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Wed, 3 Sep 2014 15:52:12 +0200
Subject: Inductive and CoInductive records are printed correctly.

---
 printing/printer.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 7971e0aaa..8c7dbac33 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -820,10 +820,17 @@ let print_record env mind mib =
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
+  let keyword =
+    let open Decl_kinds in
+    match mib.mind_finite with
+    | BiFinite -> "Record "
+    | Finite -> "Inductive "
+    | CoFinite -> "CoInductive "
+  in
   hov 0 (
     hov 0 (
       pr_polymorphic mib.mind_polymorphic ++
-      str "Record " ++ pr_id mip.mind_typename ++ brk(1,4) ++
+      str keyword ++ pr_id mip.mind_typename ++ brk(1,4) ++
       print_params env params ++
       str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
       str ":= " ++ pr_id mip.mind_consnames.(0)) ++
-- 
cgit v1.2.3