diff options
Diffstat (limited to 'src/Util/IdfunWithAlt.v')
| -rw-r--r-- | src/Util/IdfunWithAlt.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Util/IdfunWithAlt.v b/src/Util/IdfunWithAlt.v index 9754c5b24..09bb2ca76 100644 --- a/src/Util/IdfunWithAlt.v +++ b/src/Util/IdfunWithAlt.v @@ -34,8 +34,7 @@ Definition id_tuple_with_alt {A n} | O => id_with_alt | S n' => id_tuple'_with_alt end. -Fixpoint id_tuple_with_alt_proof {A n} - {struct n} +Definition id_tuple_with_alt_proof {A n} : forall (value value_for_alt : tuple A n) {pf : value = value_for_alt}, tuple A n := match n with |