aboutsummaryrefslogtreecommitdiff
path: root/printing/prettyp.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-27 10:19:29 +0100
committerMaxime Dénès2017-12-27 10:19:29 +0100
commitf6857ce53ecf64b0086854495b4a8451f476d5b4 (patch)
tree7c36a59b64fcd20b3666eca8de54b4fd33606cc1 /printing/prettyp.ml
parent4969f9425cb0d5cd5bd735110886a0cbd2641588 (diff)
parent21750c40ee3f7ef3103121db68aef4339dceba40 (diff)
Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r--printing/prettyp.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 647111bbe1..2b7886d115 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -235,8 +235,8 @@ 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 -> str" without eta conversion"
- | Decl_kinds.BiFinite -> str " with eta conversion"
+ | CoFinite | Finite -> str" without eta conversion"
+ | BiFinite -> str " with eta conversion"
in
[Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
| _ -> []