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 +++++++
 1 file changed, 7 insertions(+)

(limited to 'pretyping')

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