Add many more cases to the test-suite

I'd add more, but I'm tired and it's late and I should sleep.  Maybe
I'll pick up at 3279 (working down) another day.

Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed,
even though it raises an anomaly.  So there's no way I can think of to
test it.  I've left it in the [opened] directory anyway.

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3354.v b/test-suite/bugs/closed/3354.v
new file mode 100644
index 000000000..14b66db36
--- /dev/null
+++ b/test-suite/bugs/closed/3354.v
@@ -0,0 +1,12 @@
+Set Universe Polymorphism.
+Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
+Inductive Empty : Type1 := .
+Fail Check Empty : Set.
+(* Toplevel input, characters 15-116:
+Error: Conversion test raised an anomaly *)
+(* Now we make sure it's not an anomaly *)
+Goal True.
+Proof.
+  try exact (let x := Empty : Set in I).
+  exact I.
+Defined.