aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-07-13 17:00:25 +0200
committerPierre-Marie Pédrot2016-07-13 17:00:25 +0200
commit9f003b933c2a3504683a84ed817021659e80bc8f (patch)
tree4e9636ca44aed009d2274b03e64313c770a8b026 /printing
parent7217d14466bf900ec0353b6bbcb7e4d4b78ec2bf (diff)
parent45250332a1e65d434432940a468312f2ab18a2e8 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'printing')
-rw-r--r--printing/prettyp.ml8
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 ->