From f0449ed6183a21c65a82f59efdba3120413e3cf4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 5 Mar 2017 10:46:10 +0100
Subject: [PATCH] lrust_typing: make sum type opaque, for consistency with the
 other types

---
 theories/typing/sum.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index ef3d107d..f36ed5ae 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -249,4 +249,5 @@ End sum.
 Notation "Σ[ ty1 ; .. ; tyn ]" :=
   (sum (cons ty1%T (..(cons tyn%T nil)..))) : lrust_type_scope.
 
+Hint Opaque sum : lrust_typing lrust_typing_merge.
 Hint Resolve sum_mono' sum_proper' : lrust_typing.
-- 
GitLab