diff options
| author |  Julien Forest <julien.forest@ensiie.fr> | 2014-04-04 15:58:29 +0200 |
|---|---|---|
| committer | Julien Forest <julien.forest@ensiie.fr> | 2014-04-04 21:02:07 +0200 |
| commit | 31a69c4d0fd7b8325187e8da697a9c283594047d (patch) | |
| tree | 8f876d0abe88e2f3a3f81aa3b9d3806794e74940 /theories/Logic/FinFun.v | |
| parent | ba5efb7b2eac8fc4c2e166d0057f6c17f81c2fd6 (diff) | |
Closing bug #3164
Diffstat (limited to 'theories/Logic/FinFun.v')
| -rw-r--r-- | theories/Logic/FinFun.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v index 2f72f16de..086efb984 100644 --- a/theories/Logic/FinFun.v +++ b/theories/Logic/FinFun.v @@ -216,7 +216,7 @@ Lemma Fin_Finite n : Finite (Fin.t n). Proof. induction n. - exists nil. - inversion a. + red;inversion a. - destruct IHn as (l,Hl). exists (Fin.F1 :: map Fin.FS l). intros a. revert n a l Hl. |