From a9010048c40c85b0f5e9c5fedaf2609121e71b89 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 24 May 2016 20:32:35 +0200
Subject: primproj: warning and avoid error.

When defining a (co)recursive inductive with primitive projections on,
which lacks eta-conversion and hence dependent elimination, build only
the associated non-dependent elimination principles, and warn about
this. Also make the printing of the status of an inductive
w.r.t. projections and eta conversion explicit in Print and About.
---
 printing/prettyp.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'printing/prettyp.ml')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1f6e99c7e7..f71719cb9a 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -224,12 +224,12 @@ let print_type_in_type ref =
 let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
     let eta = match recflag with
-    | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
-    | Decl_kinds.BiFinite -> str " and has eta conversion"
+    | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion"
+    | Decl_kinds.BiFinite -> str " with eta conversion"
     in
-    [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
+    [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
   | _ -> []
-    
+
 let print_primitive ref =
   match ref with 
   | IndRef ind -> 
-- 
cgit v1.2.3