From a69bb15b1d76b71628b61bc42eb8d79c098074a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jun 2019 12:27:37 +0200
Subject: Merge universe quantification and delayed constraints in opaque
 proofs.

This enforces more invariants statically.
---
 printing/prettyp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

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)++
-- 
cgit v1.2.3