diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-28 13:47:25 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:01 +0200 |
| commit | 902da7d2949464ff54dafc3fda1d44365270d2e1 (patch) | |
| tree | e8af894bb79090b316df4fbd247e09fb464bd2ac /theories/MSets | |
| parent | 6869b22e2546b69acb74e18dc491029897ba36a3 (diff) | |
Try a new way of handling template universe levels
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetList.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 => |