Move type argument to id_tuple_with_alt outside the fixpoint

1 files changed, 26 insertions, 22 deletions

diff --git a/src/Util/IdfunWithAlt.v b/src/Util/IdfunWithAlt.v
index 09bb2ca76..8bc13019c 100644
--- a/src/Util/IdfunWithAlt.v
+++ b/src/Util/IdfunWithAlt.v
@@ -6,28 +6,32 @@ Definition id_with_alt_proof {A} (value : A) (value_for_alt : A)
            {pf : value = value_for_alt}
   : A
   := id_with_alt value value_for_alt.
-Fixpoint id_tuple'_with_alt {A n}
-         {struct n}
-  : forall (value value_for_alt : tuple' A n),
-    tuple' A n
-  := match n return forall value value_for_alt : tuple' A n, tuple' A n with
-     | O => id_with_alt
-     | S n' => fun (value value_for_alt : tuple' A n' * A)
-               => (@id_tuple'_with_alt A n' (fst value) (fst value_for_alt),
-                   @id_with_alt A (snd value) (snd value_for_alt))
-     end.
-Fixpoint id_tuple'_with_alt_proof {A n}
-         {struct n}
-  : forall (value value_for_alt : tuple' A n) {pf : value = value_for_alt},
-    tuple' A n
-  := match n return forall value value_for_alt : tuple' A n, _ -> tuple' A n with
-     | O => id_with_alt_proof
-     | S n' => fun (value value_for_alt : tuple' A n' * A) (pf : value = value_for_alt)
-               => (@id_tuple'_with_alt_proof A n' (fst value) (fst value_for_alt)
-                                             (f_equal (@fst _ _) pf),
-                   @id_with_alt_proof A (snd value) (snd value_for_alt)
-                                      (f_equal (@snd _ _) pf))
-     end.
+
+Section tuple.
+  Context {A : Type}.
+
+  Fixpoint id_tuple'_with_alt {n}
+    : forall (value value_for_alt : tuple' A n),
+      tuple' A n
+    := match n return forall value value_for_alt : tuple' A n, tuple' A n with
+       | O => id_with_alt
+       | S n' => fun (value value_for_alt : tuple' A n' * A)
+                 => (@id_tuple'_with_alt n' (fst value) (fst value_for_alt),
+                     @id_with_alt A (snd value) (snd value_for_alt))
+       end.
+
+  Fixpoint id_tuple'_with_alt_proof {n}
+    : forall (value value_for_alt : tuple' A n) {pf : value = value_for_alt},
+      tuple' A n
+    := match n return forall value value_for_alt : tuple' A n, _ -> tuple' A n with
+       | O => id_with_alt_proof
+       | S n' => fun (value value_for_alt : tuple' A n' * A) (pf : value = value_for_alt)
+                 => (@id_tuple'_with_alt_proof n' (fst value) (fst value_for_alt)
+                                               (f_equal (@fst _ _) pf),
+                     @id_with_alt_proof A (snd value) (snd value_for_alt)
+                                        (f_equal (@snd _ _) pf))
+       end.
+End tuple.
 Definition id_tuple_with_alt {A n}
   : forall (value value_for_alt : tuple A n), tuple A n
   := match n with