From bf8cda8be63a9595c6823d7c201c232aef294153 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 Feb 2015 22:01:20 +0100
Subject: [PATCH] Simplify l/r-values.

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

diff --git a/theories/listset.v b/theories/listset.v
index 00872d02..5aa61a4c 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -16,6 +16,7 @@ Instance listset_empty: Empty (listset A) := Listset [].
 Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
 Instance listset_union: Union (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (l' ++ k').
+Global Opaque listset_singleton listset_empty.
 
 Global Instance: SimpleCollection A (listset A).
 Proof.
-- 
GitLab