diff options
| author | Hugo Herbelin | 2014-08-16 17:50:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-16 17:52:53 +0200 |
| commit | 682aa67cc808e1d46b35f6f9c848946cabc226f7 (patch) | |
| tree | 9740bc148ff3a3a32293d7b29a11a802fa2d9a2f /test-suite | |
| parent | 8bc0159095cb0230a50c55a1611c8b77134a6060 (diff) | |
Fixing too restrictive detection of resolution of evars in "apply in"
(revealed by contribution PTSF).
Diffstat (limited to 'test-suite')
| -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 0d8bf5560c..71d8d26f15 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -430,3 +430,12 @@ Undo. (* H' is displayed as (forall n0, n=n0) *) apply H' with (n0:=0). Qed. + +(* Check that evars originally present in goal do not prevent apply in to work*) + +Goal (forall x, x <= 0 -> x = 0) -> exists x, x <= 0 -> 0 = 0. +intros. +eexists. +intros. +apply H in H0. +Abort. |