Fix implicit status of curry

1 files changed, 4 insertions, 4 deletions

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index cc2380d5e..2e9f7b0ad 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -103,25 +103,25 @@ Definition curryT (R T : Type) (n : nat) : Type
      | S n' => curry'T R T n'
      end.
 
-Fixpoint uncurry' R {T n} : (tuple' T n -> R) -> curry'T R T n
+Fixpoint uncurry' {R T n} : (tuple' T n -> R) -> curry'T R T n
   := match n return (tuple' T n -> R) -> curry'T R T n with
      | 0 => fun f x => f x
      | S n' => fun f => @uncurry' (T -> R) T n' (fun xs x => f (xs, x))
      end.
 
-Fixpoint uncurry R {T n} : (tuple T n -> R) -> curryT R T n
+Fixpoint uncurry {R T n} : (tuple T n -> R) -> curryT R T n
   := match n return (tuple T n -> R) -> curryT R T n with
      | 0 => fun f => f tt
      | S n' => @uncurry' R T n'
      end.
 
-Fixpoint curry' R {T n} : curry'T R T n -> (tuple' T n -> R)
+Fixpoint curry' {R T n} : curry'T R T n -> (tuple' T n -> R)
   := match n return curry'T R T n -> (tuple' T n -> R) with
      | 0 => fun f x => f x
      | S n' => fun f xs_x => @curry' (T -> R) T n' f (fst xs_x) (snd xs_x)
      end.
 
-Fixpoint curry R {T n} : curryT R T n -> (tuple T n -> R)
+Fixpoint curry {R T n} : curryT R T n -> (tuple T n -> R)
   := match n return curryT R T n -> (tuple T n -> R) with
      | 0 => fun r _ => r
      | S n' => @curry' R T n'