From 902da7d2949464ff54dafc3fda1d44365270d2e1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 28 Apr 2014 13:47:25 +0200
Subject: Try a new way of handling template universe levels

---
 theories/MSets/MSetList.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/MSets')

diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 5c232f340..fb0d1ad9d 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -56,7 +56,7 @@ Module Ops (X:OrderedType) <: WOps X.
 
   Definition singleton (x : elt) := x :: nil.
 
-  Fixpoint remove x s :=
+  Fixpoint remove x s : t :=
     match s with
     | nil => nil
     | y :: l =>
-- 
cgit v1.2.3