From e2a8edaf595827af82be67a90c0c5b22c987abe5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 22 Nov 2016 13:50:10 +0100
Subject: A refined solution to the beta-iota discrepancies between 8.4 and 8.5
 "refine".

There is a long story of commits trying to improve the compatibility
between 8.4 and 8.5 refine, as discussed in
https://github.com/coq/coq/pull/346.

ac9c5986b77bf4a783f2bd0ad571645694c960e1 add beta-iota in hypotheses and conclusion
8afac4f87d9d7e3add1c19485f475bd2207bfde7 remove beta-iota in hypotheses
08e87eb96ab67ead60d92394eec6066d9b52e55e re-add beta-iota in hypotheses
c9c54122d1d9493a965b483939e119d52121d5a6 re-remove beta-iota in hypotheses
9194180e2da0f7f9a2b2c7574bb7261cc69ead17 revert re-remove beta-iota in hypotheses
6bb352a6743c7332b9715ac15e95c806a58d101c re-re-remove beta-iota in hypotheses if <= 8.5
d8baa76d86eaa691a5386669596a6004bb44bb7a idem if = 8.5

The current commit tries to identify (one of?) the exact points of
divergence between 8.4 and 8.5 refine, namely the types inferred for
the variables of a pattern-matching problem.

Note that for the conclusion of each new goal, there were a
nf_betaiota in 8.4 done in function Evarutil.evars_to_metas, so the
compatibility expects that such a nf_betaiota on the conclusion of
each goal remains.
---
 pretyping/cases.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6bc2a4f94b..8a49cd5488 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1245,6 +1245,12 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   let typs = List.map2 RelDecl.set_name names cs_args
   in
 
+  (* Beta-iota-normalize types to better compatibility of refine with 8.4 behavior *)
+  (* This is a bit too strong I think, in the sense that what we would *)
+  (* really like is to have beta-iota reduction only at the positions where *)
+  (* parameters are substituted *)
+  let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in
+
   (* We build the matrix obtained by expanding the matching on *)
   (* "C x1..xn as x" followed by a residual matching on eqn into *)
   (* a matching on "x1 .. xn eqn" *)
-- 
cgit v1.2.3


From 9839375100365ea3bd28bfc2efdb701db7d83adb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 12:35:01 +0100
Subject: Test surgical use of beta-iota in the type of variables coming from
 pattern-matching for refine.

---
 test-suite/bugs/closed/5219.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/5219.v

diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v
new file mode 100644
index 0000000000..f7cec1a0cf
--- /dev/null
+++ b/test-suite/bugs/closed/5219.v
@@ -0,0 +1,10 @@
+(* Test surgical use of beta-iota in the type of variables coming from
+   pattern-matching for refine *)
+
+Goal forall x : sigT (fun x => x = 1), True.
+  intro x; refine match x with
+                  | existT _ x' e' => _
+                  end.
+  lazymatch goal with
+  | [ H : _ = _ |- _ ] => idtac
+  end.
-- 
cgit v1.2.3


From cc1212c3cfbd9c39cbe981210758c67cf9095be2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Apr 2017 17:25:14 +0200
Subject: Tentative note in CHANGES about now applying βι while typing "match"
 branches.

In practice, this is almost invisible except when using "refine". So,
in some sense, it is aligning the behavior of pretyping on the one of
logic.ml's "refine" so that the more natural behavior of 8.4's refine
on this issue is restored.
---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGES b/CHANGES
index 60b88ea8db..8cb5573b21 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,11 @@ Tactics
     missed before because of a missing normalization step. Hopefully this should
     be fairly uncommon.
 - "auto with real" can now discharge comparisons of literals
+- The types of variables in patterns of "match" are now
+  beta-iota-reduced after type-checking. This has an impact on the
+  type of the variables that the tactic "refine" introduces in the
+  context, producing types a priori closer to the expectations.
+
 
 Standard Library
 
-- 
cgit v1.2.3