Merge branch 'v8.6'

6 files changed, 85 insertions, 1 deletions

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.
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.
diff --git a/test-suite/bugs/closed/5331.v b/test-suite/bugs/closed/5331.v
new file mode 100644
index 0000000000..28743736d3
--- /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.
+
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index a13ae4624a..6879cbc3c2 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -10,3 +10,5 @@ let fix f (m : nat) : nat := match m with
                              end in f 0
      : nat
 Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
+     = cofix inf : Inf := {| projS := inf |}
+     : Inf
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 8afa50ba57..fafb478bad 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,4 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
   omega.
 Qed.
 
-
+CoInductive Inf := S { projS : Inf }.
+Definition expand_Inf (x : Inf) := S (projS x).
+CoFixpoint inf := S inf.
+Eval compute in inf.
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 3c696502cd..465b3eb8c0 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -41,6 +41,7 @@ Definition F (x:IND True) (A:Type) :=
 Theorem paradox : False.
   (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
 Fail Proof (F C False).
+Abort.
 
 (* Another bug found in November 2015 (a substitution was wrongly
    reversed at pretyping level) *)
@@ -61,3 +62,30 @@ Inductive Ind2 (b:=1) (c:nat) : Type :=
   Constr2 : Ind2 c.
 
 Eval vm_compute in Constr2 2.
+
+(* A bug introduced in ade2363 (similar to #5322 and #5324). This
+   commit started to see that some List.rev was wrong in the "var"
+   case of a pattern-matching problem but it failed to see that a
+   transformation from a list of arguments into a substitution was
+   still needed. *)
+
+(* The order of real arguments was made wrong by ade2363 in the "var"
+   case of the compilation of "match" *)
+
+Inductive IND2 : forall X Y:Type, Type :=
+  CONSTR2 : IND2 unit Empty_set.
+
+Check fun x:IND2 bool nat =>
+  match x in IND2 a b return a with
+  | y => _
+  end = true.
+
+(* From January 2017, using the proper function to turn arguments into
+   a substitution up to a context possibly containing let-ins, so that
+   the following, which was wrong also before ade2363, now works
+   correctly *)
+
+Check fun x:Ind bool nat =>
+  match x in Ind _ X Y Z return Z with
+  | y => (true,0)
+  end.