diff options
Diffstat (limited to 'test-suite/success/Injection.v')
-rw-r--r-- | test-suite/success/Injection.v | 2 |
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. |