diff options
| author | Hugo Herbelin | 2014-08-20 11:13:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-02 19:28:48 +0200 |
| commit | 595de46fe3de117129395157dfad28548dc0a157 (patch) | |
| tree | 02f8f0d6113db6db1fea6b5e835c999d30d96904 | |
| parent | c8528ba19efdbdf9b13d35bced7ea35048d76378 (diff) | |
An apply test.
| -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 *) |