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).
---
 pretyping/unification.ml      | 4 ++++
 test-suite/success/destruct.v | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f090921e5c..61160147ab 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -194,6 +194,10 @@ let pose_all_metas_as_evars env evd t =
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
         let ty = EConstr.of_constr ty in
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
+        let ty =
+          if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+          then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
+          else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
         let src = Evd.evar_source_of_meta mv !evdref in
         let ev = Evarutil.e_new_evar env evdref ~src ty in
         evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref;
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


From dd56ef10395a2ced84612aa799690b034306806e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 26 Jul 2017 22:34:43 +0200
Subject: Fixing another regression with 8.4 wrt to βι-normalization of created
 hyps.

This one is a continuation of e2a8edaf59 which was βι-normalizing the
hypotheses created by a "match". We forgot to do it for "let" and
"if". This is what this commit is doing.
---
 pretyping/pretyping.ml      |  7 +++++++
 test-suite/success/refine.v | 10 ++++++++++
 2 files changed, 17 insertions(+)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b4d87dfdb0..a292986bcd 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -904,6 +904,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  | [], [] -> []
 	  | _ -> assert false
 	in aux 1 1 (List.rev nal) cs.cs_args, true in
+    let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+                then Context.Rel.map (whd_betaiota !evdref) fsign
+                else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
     let obj ind p v f =
       if not record then 
         let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
@@ -1017,6 +1020,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let pi = lift n pred in (* liftn n 2 pred ? *)
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
         let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
+        let cs_args =
+          if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+          then Context.Rel.map (whd_betaiota !evdref) cs_args
+          else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in
 	let csgn =
 	  if not !allow_anonymous_refs then
 	    List.map (set_name Anonymous) cs_args
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 352abb2af5..4f6505f583 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -122,3 +122,13 @@ Abort.
 
 Goal (forall A : Prop, A -> ~~A).
 Proof. refine(fun A a f => _).
+
+(* Checking beta-iota normalization of hypotheses in created evars *)
+
+Goal {x|x=0} -> True.
+refine (fun y => let (x,a) := y in _).
+match goal with a:_=0 |- _ => idtac end.
+
+Goal (forall P, {P 0}+{P 1}) -> True.
+refine (fun H => if H (fun x => x=x) then _ else _).
+match goal with _:0=0 |- _ => idtac end.
-- 
cgit v1.2.3