10 files changed, 162 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/bug_10298.v b/test-suite/bugs/closed/bug_10298.v
new file mode 100644
index 0000000000..ad4778cc36
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10298.v
@@ -0,0 +1,35 @@
+Set Implicit Arguments.
+
+Generalizable Variables A.
+
+Parameter val : Type.
+
+Class Enc (A:Type) :=
+  make_Enc { enc : A -> val }.
+
+Global Instance Enc_dummy : Enc unit.
+Admitted.
+
+Definition FORM := forall A (EA:Enc A) (Q:A->Prop), Prop.
+
+Axiom FORM_intro : forall F : FORM, F unit Enc_dummy (fun _ : unit => True).
+
+Definition IDF (F:FORM) : FORM := F.
+
+Parameter ID : forall (G:Prop), G -> G.
+
+Parameter EID : forall A (EA:Enc A) (F:FORM) (Q:A->Prop),
+  F _ _ Q ->
+  F _ _ Q.
+
+Lemma bla : forall F,
+  (forall A (EA:Enc A), IDF F EA (fun (X:A) => True) -> True) ->
+  True.
+Proof.
+  intros F M.
+  notypeclasses refine (M _ _ _).
+  notypeclasses refine (EID _ _ _ _).
+  eapply (ID _).
+  Unshelve.
+  + apply FORM_intro.
+Qed.
diff --git a/test-suite/bugs/closed/bug_10762.v b/test-suite/bugs/closed/bug_10762.v
new file mode 100644
index 0000000000..d3991d4d38
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10762.v
@@ -0,0 +1,30 @@
+
+Set Implicit Arguments.
+
+Generalizable Variables A B.
+Parameter val: Type.
+
+Class Enc (A:Type) : Type :=
+  make_Enc { enc : A -> val }.
+
+Hint Mode Enc + : typeclass_instances.
+
+Parameter bar : forall A (EA:Enc A), EA = EA.
+
+Parameter foo : forall (P:Prop),
+   P ->
+   P = P ->
+   True.
+
+Parameter id : forall (P:Prop),
+  P -> P.
+
+  Check enc.
+
+  Lemma test : True.
+  eapply foo; [ eapply bar | apply id]. apply id.
+  (* eapply bar introduces an unresolved typeclass evar that is no longer
+     a candidate after the application (eapply should leave typeclass goals shelved).
+     We ensure that this happens also _across_ goals in `[ | ]` and not only at `.`..
+      *)
+  Abort.
diff --git a/test-suite/bugs/opened/bug_3357.v b/test-suite/bugs/opened/bug_3357.v
index c479158877..f0e5d71811 100644
--- a/test-suite/bugs/opened/bug_3357.v
+++ b/test-suite/bugs/opened/bug_3357.v
@@ -1,4 +1,9 @@
-Notation D1 := (forall {T : Type} ( x : T ) , Type).
+(* See discussion in #668 for whether manual implicit arguments should
+   be allowed in notations or not *)
+
+Set Warnings "+syntax".
+
+Fail Notation D1 := (forall {T : Type} ( x : T ) , Type).
 
 Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1.
 Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33:
diff --git a/test-suite/micromega/bug_11270.v b/test-suite/micromega/bug_11270.v
new file mode 100644
index 0000000000..80abc6d0e9
--- /dev/null
+++ b/test-suite/micromega/bug_11270.v
@@ -0,0 +1,6 @@
+Require Import Psatz.
+Theorem foo : forall a b, 1 <= S (a + a * S b).
+Proof.
+intros.
+lia.
+Qed.
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index 668be1fdbc..357afb51eb 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -56,10 +56,11 @@ Extract Constant Rinv   => "fun x -> 1 / x".
 Recursive Extraction
            Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
            Tauto.abst_form
-           ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ
+           ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
            denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+
 (* Local Variables: *)
 (* coding: utf-8 *)
 (* End: *)
diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out
new file mode 100644
index 0000000000..952761acca
--- /dev/null
+++ b/test-suite/output/print_ltac.out
@@ -0,0 +1,8 @@
+Ltac t1 := time "my tactic" idtac
+Ltac t2 := let x := string:("my tactic") in
+           idtac
+           x
+Ltac t3 := idtacstr "my tactic"
+Ltac t4 x := match x with
+             | ?A => (A, A)
+             end
diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v
new file mode 100644
index 0000000000..a992846791
--- /dev/null
+++ b/test-suite/output/print_ltac.v
@@ -0,0 +1,12 @@
+(* Testing of various things about Print Ltac *)
+(* https://github.com/coq/coq/issues/10971 *)
+Ltac t1 := time "my tactic" idtac.
+Print Ltac t1.
+Ltac t2 := let x := string:("my tactic") in idtac x.
+Print Ltac t2.
+Tactic Notation "idtacstr" string(str) := idtac str.
+Ltac t3 := idtacstr "my tactic".
+Print Ltac t3.
+(* https://github.com/coq/coq/issues/9716 *)
+Ltac t4 x := match x with ?A => constr:((A, A)) end.
+Print Ltac t4.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index d047f7560e..aa439fae12 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -165,3 +165,10 @@ Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pa
 Check fun y : nat => # (x,z) ## y & y.
 
 End M17.
+
+Module Bug10750.
+
+Notation "#" := 0 (only printing).
+Print Visibility.
+
+End Bug10750.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 23853890d8..ecaaedca53 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -124,3 +124,36 @@ Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
 (* Check global implicit declaration over ref not in section *)
 
 Section D. Global Arguments eq [A] _ _. End D.
+
+(* Check local manual implicit arguments *)
+(* Gives a warning and make the second x anonymous *)
+(* Isn't the name "arg_1" a bit fragile though? *)
+
+Check fun f : forall {x:nat} {x:bool} (x:unit), unit => f (x:=1) (arg_2:=true) tt.
+
+(* Check the existence of a shadowing warning *)
+
+Set Warnings "+syntax".
+Fail Check fun f : forall {x:nat} {x:bool} (x:unit), unit => f (x:=1) (arg_2:=true) tt.
+Set Warnings "syntax".
+
+(* Test failure when implicit arguments are mentioned in subterms
+   which are not types of variables *)
+
+Set Warnings "+syntax".
+Fail Check (id (forall {a}, a)).
+Set Warnings "syntax".
+
+(* Miscellaneous tests *)
+
+Check let f := fun {x:nat} y => y=true in f false.
+
+(* Isn't the name "arg_1" a bit fragile, here? *)
+
+Check fun f : forall {_:nat}, nat => f (arg_1:=0).
+
+(* This test was wrongly warning/failing at some time *)
+
+Set Warnings "+syntax".
+Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
+Set Warnings "syntax".
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index f12db8b081..1b04594290 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -109,6 +109,28 @@ match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
 
+(* let ins should be supported in the type of the specialized hypothesis *)
+Axiom foo: forall (m1 m2: nat), let n := 2 * m1 in m1 = m2 -> False.
+Goal False.
+  pose proof foo as P.
+  assert (2 = 2) as A by reflexivity.
+  specialize P with (1 := A).
+  assumption.
+Qed.
+
+(* Another more subtle test on letins: they should not interfere with foralls. *)
+Goal forall (P: forall y:nat,
+                forall A (zz:A),
+                  let a := zz in
+                  let x := 1 in
+                  forall n : y = x,
+                    n = n),
+    True.
+  intros P.
+  specialize P with (zz := @eq_refl _ 2).
+  constructor.
+Qed.
+
 (* Test specialize as *)
 
 Goal (forall x, x=0) -> 1=0.