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].

1 files changed, 2 insertions, 2 deletions

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.