7 files changed, 221 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/148.v b/test-suite/bugs/closed/148.v
new file mode 100644
index 0000000000..6cafb9f0cd
--- /dev/null
+++ b/test-suite/bugs/closed/148.v
@@ -0,0 +1,26 @@
+(** Omega is now aware of the bodies of context variables
+    (of type Z or nat). *)
+
+Require Import ZArith Omega.
+Open Scope Z.
+
+Goal let x := 3 in x = 3.
+intros.
+omega.
+Qed.
+
+Open Scope nat.
+
+Goal let x := 2 in x = 2.
+intros.
+omega.
+Qed.
+
+(** NB: this could be disabled for compatibility reasons *)
+
+Unset Omega UseLocalDefs.
+
+Goal let x := 4 in x = 4.
+intros.
+Fail omega.
+Abort.
diff --git a/test-suite/bugs/closed/4852.v b/test-suite/bugs/closed/4852.v
new file mode 100644
index 0000000000..5068ed9b95
--- /dev/null
+++ b/test-suite/bugs/closed/4852.v
@@ -0,0 +1,54 @@
+(** BZ 4852 : unsatisfactory Extraction Implicit for a fixpoint defined via wf *)
+
+Require Import Coq.Lists.List.
+Import ListNotations.
+Require Import Omega.
+
+Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf.
+
+Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) :=
+  let R := fresh in
+  let E := fresh in
+  remember term as R eqn:E;
+  revert E; revert Hs;
+  induction R as [R H] using wfi_lt;
+  intros; subst R.
+
+Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws.
+
+Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega.
+
+Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'").
+
+Definition split_acc (ls : list nat) : forall acc1 acc2,
+    (|acc1| = |acc2| \/ |acc1| = S (|acc2|)) ->
+    { lss : list nat * list nat |
+      let '(ls1, ls2) := lss in |ls1++ls2| = |ls++acc1++acc2| /\ (|ls1| = |ls2| \/ |ls1| = S (|ls2|))}.
+Proof.
+  induction ls as [|a ls IHls]. all:intros acc1 acc2 H.
+  { exists (acc1, acc2). cbn. intuition reflexivity. }
+  destruct (IHls (a::acc2) acc1) as [[ls1 ls2] (H1 & H2)]. 1:solve_nat.
+  exists (ls1, ls2). cbn. intuition solve_nat.
+Defined.
+
+Definition join(ls : list nat) : { rls : list nat | |rls| = |ls| }.
+Proof.
+  wfinduction (|ls|) on ls as IH.
+  case (split_acc ls [] []). 1:solve_nat.
+  intros (ls1 & ls2) (H1 & H2).
+  destruct ls2 as [|a ls2].
+  - exists ls1. solve_nat.
+  - unshelve eelim (IH _ _ ls1 eq_refl). 1:solve_nat. intros rls1 H3.
+    unshelve eelim (IH _ _ ls2 eq_refl). 1:solve_nat. intros rls2 H4.
+    exists (a :: rls1 ++ rls2). solve_nat.
+Defined.
+
+Require Import ExtrOcamlNatInt.
+Extract Inlined Constant length => "List.length".
+Extract Inlined Constant app => "List.append".
+
+Extraction Inline wfi_lt.
+Extraction Implicit wfi_lt [1 3].
+Recursive Extraction join. (* was: Error: An implicit occurs after extraction *)
+Extraction TestCompile join.
+
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/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.
diff --git a/test-suite/bugs/closed/5765.v b/test-suite/bugs/closed/5765.v
new file mode 100644
index 0000000000..343ab49357
--- /dev/null
+++ b/test-suite/bugs/closed/5765.v
@@ -0,0 +1,3 @@
+(* 'pat binder not (yet?) allowed in parameters of inductive types *)
+
+Fail Inductive X '(a,b) := x.
diff --git a/test-suite/bugs/closed/5769.v b/test-suite/bugs/closed/5769.v
new file mode 100644
index 0000000000..42573aad87
--- /dev/null
+++ b/test-suite/bugs/closed/5769.v
@@ -0,0 +1,20 @@
+(* Check a few naming heuristics based on types *)
+(* was buggy for types names _something *)
+
+Inductive _foo :=.
+Lemma bob : (sigT (fun x : nat => _foo)) -> _foo.
+destruct 1.
+exact _f.
+Abort.
+
+Inductive _'Foo :=.
+Lemma bob : (sigT (fun x : nat => _'Foo)) -> _'Foo.
+destruct 1.
+exact _'f.
+Abort.
+
+Inductive ____ :=.
+Lemma bob : (sigT (fun x : nat => ____)) -> ____.
+destruct 1.
+exact x0.
+Abort.