From 7bda7d7070fc55fc38fef4c21557ea61b0c4d17d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 9 Jul 2015 14:50:16 +0900
Subject: Fixing printing of primitive coinductive record status.

They do not have eta-rule indeed, even though it was displayed as such.
---
 printing/prettyp.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e50435cda2..b8c5fd4cfc 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -205,16 +205,20 @@ let print_polymorphism ref =
        else "not universe polymorphic") ]
   else []
 
-let print_primitive_record mipv = function
+let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
-    [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."]
+    let eta = match recflag with
+    | Decl_kinds.CoFinite -> mt ()
+    | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+    in
+    [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
   | _ -> []
     
 let print_primitive ref =
   match ref with 
   | IndRef ind -> 
     let mib,_ = Global.lookup_inductive ind in
-      print_primitive_record mib.mind_packets mib.mind_record
+      print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record
   | _ -> []
 
 let print_name_infos ref =
@@ -447,7 +451,7 @@ let gallina_print_inductive sp =
   let mipv = mib.mind_packets in
   pr_mutual_inductive_body env sp mib ++
   with_line_skip
-    (print_primitive_record mipv mib.mind_record @
+    (print_primitive_record mib.mind_finite mipv mib.mind_record @
      print_inductive_renames sp mipv @
      print_inductive_implicit_args sp mipv @
      print_inductive_argument_scopes sp mipv)
-- 
cgit v1.2.3