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.