From 9490c6099e1da94fcf315aba48125993cd180327 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 26 Jul 2017 22:29:23 +0200
Subject: 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).
---
 test-suite/success/destruct.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3