diff options
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | theories/Logic/FinFun.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 28ca7edb57..74661b836f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -596,7 +596,7 @@ let intros_until_gen red h = Tacticals.New.tclDO n (if red then introf else intro) end -let intros_until_id id = intros_until_gen true (NamedHyp id) +let intros_until_id id = intros_until_gen false (NamedHyp id) let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) let intros_until = intros_until_gen true diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v index 2f72f16dea..086efb9841 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. |