aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/prettyp.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b7b1d67f03..9745a79250 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -218,8 +218,8 @@ let print_polymorphism ref =
let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
let eta = match recflag with
- | Decl_kinds.CoFinite -> mt ()
- | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+ | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
+ | Decl_kinds.BiFinite -> str " and has eta conversion"
in
[pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
| _ -> []