Add missing test-suite files and update gitignore.

4 files changed, 30 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
index 54b9d10b5..c0bae6c66 100644
--- a/.gitignore
+++ b/.gitignore
@@ -160,3 +160,6 @@ dev/myinclude
 
 # coqide generated files (when testing)
 *.crashcoqide
+/doc/refman/Reference-Manual.hoptind
+/doc/refman/Reference-Manual.optidx
+/doc/refman/Reference-Manual.optind
diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v
new file mode 100644
index 000000000..51d6744c5
--- /dev/null
+++ b/test-suite/bugs/closed/3590.v
@@ -0,0 +1,14 @@
+(* Set Primitive Projections. *)
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Definition idS := Set.
+Goal forall x y : prod Set Set, fst x = fst y.
+  intros.
+  change (@fst _ _ ?z) with (@fst Set idS z) at 2.
+  Unshelve.
+  admit.
+Qed.
+  
+(* Toplevel input, characters 20-58:
+Error: Failed to get enough information from the left-hand side to type the
+right-hand side. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4046.v b/test-suite/bugs/closed/4046.v
new file mode 100644
index 000000000..8f8779b7b
--- /dev/null
+++ b/test-suite/bugs/closed/4046.v
@@ -0,0 +1,6 @@
+Module Import Foo.
+  Class Foo := { foo : Type }.
+End Foo.
+
+Instance f : Foo := { foo := nat }. (* works fine *)
+Instance f' : Foo.Foo := { Foo.foo := nat }. 
diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v
new file mode 100644
index 000000000..511a92b2a
--- /dev/null
+++ b/test-suite/bugs/opened/3794.v
@@ -0,0 +1,7 @@
+Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate.
+Hint Unfold not : core.
+
+Goal true<>false.
+Set Typeclasses Debug.
+typeclasses eauto with core.
+Qed.
\ No newline at end of file