More test-suite cases

1 files changed, 26 insertions, 12 deletions

diff --git a/test-suite/bugs/closed/3373.v b/test-suite/bugs/closed/3373.v
index 16b137091..5ecf28015 100644
--- a/test-suite/bugs/closed/3373.v
+++ b/test-suite/bugs/closed/3373.v
@@ -5,15 +5,29 @@ from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348
 lines to 320 lines, then from 328 lines to 302 lines, then from 332 lines to 21
 lines *)
 Set Universe Polymorphism.
-Axiom admit : forall {T}, T.
-Definition UU := Set.
-Definition UU' := Type.
-Definition hSet:= sigT (fun X : UU' => admit) .
-Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type.
-Coercion pr1hSet: hSet >-> Sortclass.
-Axiom binop : UU -> Type.
-Axiom setwithbinop : Type.
-Definition pr1setwithbinop : setwithbinop -> hSet.
-Goal True.
-pose (( @projT1 _ ( fun X : hSet@{Set j k} => binop X ) ) : _ -> hSet).
-Admitted.
\ No newline at end of file
+Module short.
+  Record foo := { bar : Type }.
+  Coercion baz (x : foo@{Set}) : Set := bar x.
+  Goal True.
+  Proof.
+    Fail pose ({| bar := Set |} : Type). (* check that it fails *)
+    try pose ({| bar := Set |} : Type). (* Anomaly: apply_coercion_args: mismatch between arguments and coercion.
+Please report. *)
+  Admitted.
+End short.
+
+Module long.
+  Axiom admit : forall {T}, T.
+  Definition UU := Set.
+  Definition UU' := Type.
+  Definition hSet:= sigT (fun X : UU' => admit) .
+  Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type.
+  Coercion pr1hSet: hSet >-> Sortclass.
+  Axiom binop : UU -> Type.
+  Axiom setwithbinop : Type.
+  Goal True.
+  Proof.
+    Fail pose (( @projT1 _ ( fun X : hSet@{i j k} => binop X ) ) : _ -> hSet). (* check that it fails *)
+    try pose (( @projT1 _ ( fun X : hSet@{i j k} => binop X ) ) : _ -> hSet). (* check that it's not an anomaly *)
+  Admitted.
+End long.