From e91ae93106b6bd6d92ef53ac18b04654485a8106 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Jan 2017 10:52:18 +0100
Subject: Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs
 with let-ins).

A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing
a matching over a "catch-all" variable, when let-ins occur in the
arity. However ade2363e35 failed to understand what was the correct
fix, introducing instead the regressions mentioned in #5322 and #5324.

This fixes all of #5322 and #5324, as well as the handling of let-ins
in the arity.

Thanks to Jason for helping in diagnosing the problem.
---
 test-suite/bugs/closed/5322.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/bugs/closed/5322.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5322.v b/test-suite/bugs/closed/5322.v
new file mode 100644
index 0000000000..01aec8f29b
--- /dev/null
+++ b/test-suite/bugs/closed/5322.v
@@ -0,0 +1,14 @@
+(* Regression in computing types of branches in "match" *)
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := a : op Unit Unit.
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2.
+  refine match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with
+         | _ => _
+         end.
-- 
cgit v1.2.3


From a6f687852c0c7509a06fdf16c0af29129b3566d5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Jan 2017 10:32:08 +0100
Subject: Fixing unification regression #5323.

Tracking conversion problems to reconsider was lost for evars subject
to restriction (field last_mods was not updated and conversion
problems not considered to be changed).
---
 test-suite/bugs/closed/5323.v | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 test-suite/bugs/closed/5323.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5323.v b/test-suite/bugs/closed/5323.v
new file mode 100644
index 0000000000..295b7cd9f5
--- /dev/null
+++ b/test-suite/bugs/closed/5323.v
@@ -0,0 +1,26 @@
+(* Revealed a missing re-consideration of postponed problems *)
+
+Module A.
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type 
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := .
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2
+  := match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with end.
+End A.
+
+(* A shorter variant *)
+Module B.
+Inductive exprf (op : unit -> Type) : Type :=
+| A : exprf op
+| Op tR (opc : op tR) (args : exprf op) : exprf op.
+Inductive op : unit -> Type := .
+Definition bound_op (dst2 : unit) (opc2 : op dst2)
+  : forall (args2 : exprf op), Op op dst2 opc2 args2 = A op
+  := match opc2 in op h return (forall args2 : exprf ?[U], Op ?[V] ?[I] opc2 args2 = A op) with end.
+End B.
-- 
cgit v1.2.3


From f5923c2174fbb419397f127af31ab1cd0b223e0a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 31 Jan 2017 06:36:25 +0100
Subject: Fixing #5311 (anomaly on unexpected intro pattern).

This was introduced in 8.5 while reorganizing the structure of
intro-patterns.
---
 test-suite/bugs/closed/5331.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/5331.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/5331.v b/test-suite/bugs/closed/5331.v
new file mode 100644
index 0000000000..0d72fcb5df
--- /dev/null
+++ b/test-suite/bugs/closed/5331.v
@@ -0,0 +1,11 @@
+(* Checking no anomaly on some unexpected intropattern *)
+
+Ltac ih H := induction H as H.
+Ltac ih' H H' := induction H as H'.
+
+Goal True -> True.
+Fail intro H; ih H.
+intro H; ih' H ipattern:[].
+exact I.
+Qed.
+
-- 
cgit v1.2.3