diff options
| author | Hugo Herbelin | 2017-07-26 22:29:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-08-21 12:38:09 +0200 |
| commit | 9490c6099e1da94fcf315aba48125993cd180327 (patch) | |
| tree | 4a73cd1032b6ae47ca094b67fa20de29d38adf5d /test-suite | |
| parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) | |
Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps.
Formerly, mk_refgoals in logic.ml was applying full βι on new Meta-based goals.
We simulate part of this βι-normalization in pose_all_metas_as_evars.
I suspect that we don't βι-normalize goals more than in 8.4 by doing
that, since all Metas would have eventually gone to mk_refgoals, but
difficult to know for sure as there were probably metas turned to
evars (and hence a priori not βι-normalized) even when logic.ml was
used more pervasively.
However, βι-normalizing is a priori a better heuristic than no
βι-normalizing, independently of what it was in 8.4 and before (even
if, ideally, I would personally lean towards preferring a
"chirurgical" substitution with reduction only at the place of
substitution).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 90a60daa66..ea939f0855 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -430,3 +430,9 @@ eexists ?[x]. destruct (S _). change (0 = ?x). Abort. + +Goal (forall P, P 0 -> True/\True) -> True. +intro H. +destruct (H (fun x => True)). +match goal with |- True => idtac end. +Abort. |