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.

1 files changed, 4 insertions, 4 deletions

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 ->