Merge branch 'primproj' into v8.6

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