From 9e6105ece0d7c71c496752c8025b71732172f5e4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 15 Jan 2017 14:00:30 -0500 Subject: Fix an issue with universes We don't want to force the universe of [option] below other universes; to get template polymorphism to refresh universes, we need to eta-expand [option]. --- src/Util/Tuple.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index a5b299ac0..b97bfbc49 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -392,9 +392,9 @@ Local Notation option_bind | None => None end). Definition lift_option {n A} (xs : tuple (option A) n) : option (tuple A n) - := lift_monad option option_bind (@Some) xs. + := lift_monad (fun T => option T) option_bind (@Some) xs. Definition push_option {n A} (xs : option (tuple A n)) : tuple (option A) n - := push_monad option option_bind (@Some) xs. + := push_monad (fun T => option T) option_bind (@Some) xs. Lemma lift_push_option {n A} (xs : option (tuple A (S n))) : lift_option (push_option xs) = xs. Proof. -- cgit v1.2.3