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, 47 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3324.v b/test-suite/bugs/closed/3324.v
new file mode 100644
index 000000000..9cd6e4c2e
--- /dev/null
+++ b/test-suite/bugs/closed/3324.v
@@ -0,0 +1,47 @@
+Module ETassi.
+  Axiom admit : forall {T}, T.
+  Class IsHProp (A : Type) : Type := {}.
+  Class IsHSet (A : Type) : Type := {}.
+  Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
+  Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+  Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
+  Global Instance isset_hProp : IsHSet hProp | 0.
+
+  Check (eq_refl _ : setT (default_HSet _ _) = hProp).
+  Check (eq_refl _ : setT _ = hProp).
+End ETassi.
+
+Module JGross.
+  (* File reduced by coq-bug-finder from original input, then from 6462 lines to 5760 lines, then from 5761 lines to 181 lines, then from 191 lines to 181 lines, then from 181 lines to 83 lines, then from 87 lines to 27 lines *)
+  Axiom admit : forall {T}, T.
+  Class IsHProp (A : Type) : Type := {}.
+  Class IsHSet (A : Type) : Type := {}.
+  Inductive Unit : Set := tt.
+  Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
+  Definition Unit_hp:hProp:=(hp Unit admit).
+  Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+  Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
+  Global Instance isset_hProp : IsHSet hProp | 0.
+  Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
+                                      forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
+  Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> True.
+  Proof.
+    intros epif.
+    set (g :=fun _:Y => Unit_hp).
+    pose proof (epif (default_HSet hProp isset_hProp) g).
+    specialize (epif _ g).
+    (* Toplevel input, characters 34-35:
+Error:
+In environment
+X : Type
+Y : Type
+f : X -> Y
+epif : isepi f
+g := fun _ : Y => Unit_hp : Y -> hProp
+H : forall h : Y -> default_HSet hProp isset_hProp,
+    (fun x : X => g (f x)) = (fun x : X => h (f x)) -> g = h
+The term "g" has type "Y -> hProp" while it is expected to have type
+ "Y -> ?30".
+     *)
+  Abort.
+End JGross.