"Let in" in pattern hell, one more iteration

This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf.

An other wrong externalize function

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index da5dd5e402..59aa87de4e 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -17,7 +17,7 @@ Check
  fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
    let B := A in
      fun (a : A) (e : eq1 A a) =>
-       match e in (eq1 A0 B0 a0) return (P A0 a0) with
+       match e in (@eq1 A0 B0 a0) return (P A0 a0) with
        | refl1 => f
        end.
 
@@ -37,7 +37,7 @@ Check
    fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type)
      (f : forall z : C, P z (I C D x y z)) (y0 : C)
      (a : A C D x y y0) =>
-   match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with
+   match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with
    | I x0 => f x0
    end).
 
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index b24ed2f1b6..01ebfc4f04 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -25,7 +25,7 @@ Check
  fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
    let B := A in
      fun (a : A) (e : eq1 A a) =>
-       match e in (eq1 A0 B0 a0) return (P A0 a0) with
+       match e in (eq1 A0 a0) return (P A0 a0) with
        | refl1 => f
        end.