diff options
| -rw-r--r-- | test-suite/success/apply.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 29c9ab95ff..48db9c41cf 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -463,6 +463,15 @@ Abort. Goal forall H:0=0, H = H. intros. Fail apply eq_sym in H. + +(* Check that unresolved evars not originally present in goal prevent + apply in to work*) + +Goal (forall x y, x <= 0 -> x + y = 0) -> exists x, x <= 0 -> 0 = 0. +intros. +eexists. +intros. +Fail apply H in H0. Abort. (* Check naming pattern in apply in *) |