From 31a69c4d0fd7b8325187e8da697a9c283594047d Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Fri, 4 Apr 2014 15:58:29 +0200
Subject: Closing bug #3164

---
 tactics/tactics.ml      | 2 +-
 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.
-- 
cgit v1.2.3