3 files changed, 41 insertions, 1 deletions
diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v
new file mode 100644
index 0000000000..ed035f5213
--- /dev/null
+++ b/test-suite/success/BracketsWithGoalSelector.v
@@ -0,0 +1,16 @@
+Goal forall A B, B \/ A -> A \/ B.
+Proof.
+  intros * [HB | HA].
+  2: {
+    left.
+    exact HA.
+    Fail right. (* No such goal. Try unfocusing with "}". *)
+  }
+  Fail 2: { (* Non-existent goal. *)
+    idtac. (* The idtac is to get a dot, so that IDEs know to stop there. *)
+  1:{ (* Syntactic test: no space before bracket. *)
+    right.
+    exact HB.
+Fail Qed.
+  }
+Qed.
diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v
index b736b734fd..aa8da53361 100644
--- a/test-suite/success/abstract_poly.v
+++ b/test-suite/success/abstract_poly.v
@@ -17,4 +17,4 @@ intros m n P e p.
 abstract (rewrite e in p; exact p).
 Defined.
 
-Check bar_subproof@{Set Set Set}.
+Check bar_subproof@{Set Set}.
diff --git a/test-suite/success/dtauto-let-deps.v b/test-suite/success/dtauto-let-deps.v
new file mode 100644
index 0000000000..094b2f8b3c
--- /dev/null
+++ b/test-suite/success/dtauto-let-deps.v
@@ -0,0 +1,24 @@
+(*
+This test is sensitive to changes in which let-ins are expanded when checking
+for dependencies in constructors.
+If the (x := X) is not reduced, Foo1 won't be recognized as a conjunction,
+and if the (y := X) is reduced, Foo2 will be recognized as a conjunction.
+
+This tests the behavior of engine/termops.ml : prod_applist_assum,
+which is currently specified to reduce exactly the parameters.
+
+If dtauto is changed to reduce lets in constructors before checking dependency,
+this test will need to be changed.
+*)
+
+Context (P Q : Type).
+Inductive Foo1 (X : Type) (x := X) := foo1 : let y := X in P -> Q -> Foo1 x.
+Inductive Foo2 (X : Type) (x := X) := foo2 : let y := X in P -> Q -> Foo2 y.
+
+Goal P -> Q -> Foo1 nat.
+solve [dtauto].
+Qed.
+
+Goal P -> Q -> Foo2 nat.
+Fail solve [dtauto].
+Abort.