5 files changed, 88 insertions, 0 deletions
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/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.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 65efe228af..6ef75dd135 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -124,3 +124,7 @@ return (1, 2, 3, 4)
      : nat
 !!! _ _ : nat, True
      : (nat -> Prop) * ((nat -> Prop) * Prop)
+((*1).2).3
+     : nat
+*(1.2)
+     : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ea372ad1a3..8c7bbe5917 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -190,3 +190,10 @@ Check 1+1+1.
 (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
 Check !!! (x y:nat), True.
+
+(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
+
+Notation "* x" := (id x) (only printing, at level 15, format "* x").
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Check (((id 1) + 2) + 3).
+Check (id (1 + 2)).