6 files changed, 155 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v
new file mode 100644
index 0000000000..55ef7abe40
--- /dev/null
+++ b/test-suite/bugs/closed/5692.v
@@ -0,0 +1,38 @@
+Set Primitive Projections.
+Require Import ZArith ssreflect.
+
+Module Test3.
+
+Set Primitive Projections.
+
+Structure semigroup := SemiGroup {
+  sg_car :> Type;
+  sg_op : sg_car -> sg_car -> sg_car;
+}.
+
+Structure group := Something {
+  group_car :> Type;
+  group_op : group_car -> group_car -> group_car;
+  group_neg : group_car -> group_car;
+  group_neg_op' x y : group_neg (group_op x y) = group_op (group_neg x) (group_neg y)
+}.
+
+Coercion group_sg (X : group) : semigroup :=
+  SemiGroup (group_car X) (group_op X).
+Canonical Structure group_sg.
+
+Axiom group_neg_op : forall (X : group) (x y : X),
+  group_neg X (sg_op (group_sg X) x y) = sg_op (group_sg X) (group_neg X x) (group_neg X y).
+
+Canonical Structure Z_sg := SemiGroup Z Z.add .
+Canonical Structure Z_group := Something Z Z.add Z.opp Z.opp_add_distr.
+
+Lemma foo (x y : Z) :
+  sg_op Z_sg (group_neg Z_group x) (group_neg Z_group y) =
+  group_neg Z_group (sg_op Z_sg x y).
+Proof.
+  rewrite -group_neg_op.
+  reflexivity.
+Qed.
+
+End Test3.
diff --git a/test-suite/bugs/closed/5741.v b/test-suite/bugs/closed/5741.v
new file mode 100644
index 0000000000..f6598f192d
--- /dev/null
+++ b/test-suite/bugs/closed/5741.v
@@ -0,0 +1,4 @@
+(* Check no anomaly in info_trivial *)
+
+Goal True.
+info_trivial.
diff --git a/test-suite/bugs/closed/5749.v b/test-suite/bugs/closed/5749.v
new file mode 100644
index 0000000000..81bfe351c5
--- /dev/null
+++ b/test-suite/bugs/closed/5749.v
@@ -0,0 +1,18 @@
+(* Checking computation of free vars of a term for generalization *)
+
+Definition Decision := fun P : Prop => {P} + {~ P}.
+Class SetUnfold (P Q : Prop) : Prop := Build_SetUnfold { set_unfold : P <-> Q
+}.
+
+Section Filter_Help.
+
+  Context {A: Type}.
+  Context (fold_right : forall A B : Type, (B -> A -> A) -> A -> list B -> A).
+  Definition lType2 := (sigT (fun (P : A -> Prop) => forall a, Decision (P
+a))).
+  Definition test (X: lType2) := let (x, _) := X in x.
+
+  Global Instance foo `{fhl1 : list lType2} m Q:
+    SetUnfold (Q)
+              (fold_right _ _ (fun (s : lType2) => let (P, _) := s in and (P
+m)) (Q) (fhl1)).
diff --git a/test-suite/bugs/closed/5750.v b/test-suite/bugs/closed/5750.v
new file mode 100644
index 0000000000..6d0e21f5d0
--- /dev/null
+++ b/test-suite/bugs/closed/5750.v
@@ -0,0 +1,3 @@
+(* Check printability of the hole of the context *)
+Goal 0 = 0.
+match goal with |- context c [0] => idtac c end.
diff --git a/test-suite/bugs/closed/5755.v b/test-suite/bugs/closed/5755.v
new file mode 100644
index 0000000000..e07fdcf831
--- /dev/null
+++ b/test-suite/bugs/closed/5755.v
@@ -0,0 +1,16 @@
+(* Sections taking care of let-ins for inductive types *)
+
+Section Foo.
+
+Inductive foo (A : Type) (x : A) (y := x) (y : A) := Foo.
+
+End Foo.
+
+Section Foo2.
+
+Variable B : Type.
+Variable b : B.
+Let c := b.
+Inductive foo2 (A : Type) (x : A) (y := x) (y : A) := Foo2 : c=c -> foo2 A x y.
+
+End Foo2.
diff --git a/test-suite/bugs/closed/5757.v b/test-suite/bugs/closed/5757.v
new file mode 100644
index 0000000000..0d0f2eed44
--- /dev/null
+++ b/test-suite/bugs/closed/5757.v
@@ -0,0 +1,76 @@
+(* Check that resolved status of evars follows "restrict" *)
+
+Axiom H : forall (v : nat), Some 0 = Some v -> True.
+Lemma L : True.
+eapply H with _;
+match goal with
+  | |- Some 0 = Some ?v => change (Some (0+0) = Some v)
+end.
+Abort.
+
+(* The original example *)
+
+Set Default Proof Using "Type".
+
+Module heap_lang.
+
+Inductive expr :=
+  | InjR (e : expr).
+
+Inductive val :=
+  | InjRV (v : val).
+
+Bind Scope val_scope with val.
+
+Fixpoint of_val (v : val) : expr :=
+  match v with
+  | InjRV v => InjR (of_val v)
+  end.
+
+Fixpoint to_val (e : expr) : option val := None.
+
+End heap_lang.
+Export heap_lang.
+
+Module W.
+Inductive expr :=
+  | Val (v : val)
+  (* Sums *)
+  | InjR (e : expr).
+
+Fixpoint to_expr (e : expr) : heap_lang.expr :=
+  match e with
+  | Val v => of_val v
+  | InjR e => heap_lang.InjR (to_expr e)
+  end.
+
+End W.
+
+
+
+Section Tests.
+
+  Context (iProp: Type).
+  Context (WPre: expr -> Prop).
+
+  Context (tac_wp_alloc :
+             forall (e : expr) (v : val),
+               to_val e = Some v -> WPre e).
+
+  Lemma push_atomic_spec (x: val) :
+    WPre (InjR (of_val x)).
+  Proof.
+(* This works. *)
+eapply tac_wp_alloc with _.
+match goal with
+  | |- to_val ?e = Some ?v =>
+    change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
+end.
+Undo. Undo.
+(* This is fixed *)
+eapply tac_wp_alloc with _;
+match goal with
+  | |- to_val ?e = Some ?v =>
+    change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
+end.
+Abort.