aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/prettyp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 396c954b42..65197edb9d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -587,7 +587,7 @@ let print_constant with_values sep sp udecl =
| Some (c, priv, ctx) ->
let priv = match priv with
| Opaqueproof.PrivateMonomorphic () -> None
- | Opaqueproof.PrivatePolymorphic ctx -> Some ctx
+ | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx
in
print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++