From 71dd8f63e89f15926d8226de62bdff14d7d358a8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Feb 2016 15:20:30 +0100
Subject: [PATCH] make fn_cons universe polymorphic... otherwise, I run into
 universe errors :-/

---
 prelude/functions.v | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/prelude/functions.v b/prelude/functions.v
index bc12965f0..193c37659 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -31,23 +31,19 @@ Section functions.
 End functions.
 
 (** "Cons-ing" of functions from nat to T *)
-Section fcons.
-  Context {T : Type}.
+Polymorphic Definition fn_cons {T : Type} (t : T) (f: nat → T) : nat → T :=
+  λ n, match n with
+       | O => t
+       | S n => f n
+       end.
 
-  Definition fn_cons (t : T) (f: nat → T) : nat → T :=
-    λ n, match n with
-         | O => t
-         | S n => f n
-         end.
-
-  Definition fn_mcons (ts : list T) (f : nat → T) : nat → T :=
+Polymorphic Definition fn_mcons {T : Type} (ts : list T) (f : nat → T) : nat → T :=
     fold_right fn_cons f ts.
-End fcons.
 
 Infix ".::" := fn_cons (at level 60, right associativity) : C_scope.
 Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope.
 
-Lemma fn_mcons_app {T : Type} (ts1 ts2 : list T) f :
+Polymorphic Lemma fn_mcons_app {T : Type} (ts1 ts2 : list T) f :
   (ts1 ++ ts2) .++ f = ts1 .++ (ts2 .++ f).
 Proof.
   unfold fn_mcons. rewrite fold_right_app. done.
-- 
GitLab