aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Injection.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/Injection.v')
-rw-r--r--test-suite/success/Injection.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 8fd039462..56ed89ed8 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -70,7 +70,7 @@ Abort.
Goal (forall x y : nat, x = y -> S x = S y) -> True.
intros.
-einjection (H O) as H0.
+einjection (H O ?[y]) as H0.
instantiate (y:=O).
Abort.