Fixed some HoTT bugs, provide a proper error message when giving an ill-formed

universe instance.

4 files changed, 1 insertions, 114 deletions

diff --git a/test-suite/bugs/opened/3372.v b/test-suite/bugs/opened/3372.v
index 41ee400fd9..13ce75b84c 100644
--- a/test-suite/bugs/opened/3372.v
+++ b/test-suite/bugs/opened/3372.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
 Definition hProp : Type := sigT (fun _ : Type => True).
-Fail Goal hProp@{Set}. (* Toplevel input, characters 15-32:
+Goal hProp@{Set}. (* Toplevel input, characters 15-32:
 Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
 Please report. *)
diff --git a/test-suite/bugs/opened/3373.v b/test-suite/bugs/opened/3373.v
deleted file mode 100644
index 8b3b515678..0000000000
--- a/test-suite/bugs/opened/3373.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then 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.
-Fail exact ( @projT1 _ ( fun X : hSet@{i j} => binop X ) ).
-(* Toplevel input, characters 15-69:
-Anomaly: apply_coercion_args: mismatch between arguments and coercion.
-Please report. *)
diff --git a/test-suite/bugs/opened/3374.v b/test-suite/bugs/opened/3374.v
deleted file mode 100644
index 8a62838f06..0000000000
--- a/test-suite/bugs/opened/3374.v
+++ /dev/null
@@ -1,50 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then 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 331 lines to 59 lines *)
-
-Set Universe Polymorphism.
-Axiom admit : forall {T}, T.
-Notation paths := identity .
-Definition UU := Set.
-Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) .
-Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) .
-Definition hProp := sigT (fun X : Type => admit).
-Definition hProptoType := @projT1 _ _ : hProp -> Type .
-Coercion hProptoType: hProp >-> Sortclass.
-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 hsubtypes : UU -> Type.
-Definition hrel ( X : UU ) := X -> X -> hProp.
-Axiom hreldirprod : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ), hrel ( dirprod X Y ) .
-Axiom iseqclass : forall { X : UU } ( R : hrel X ) ( A : hsubtypes X ), Type.
-Definition setquot { X : UU } ( R : hrel X ) : Type := sigT (fun A => iseqclass R A).
-Axiom dirprodtosetquot : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ),
-                           setquot ( hreldirprod RX RY ).
-Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y )
-  := forall x x' x0 x0' : X , R x x' ->  R x0 x0' ->  paths ( f x x0 ) ( f x' x0' ) .
-Axiom setquotuniv : forall  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ), Y .
-Definition setquotuniv2  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R )
-: Y .
-Proof.
-  intros .
-  set ( RR := hreldirprod R R ) .
-  apply (setquotuniv RR Y admit).
-  apply (dirprodtosetquot R R).
-  apply dirprodpair; [ exact c | exact c0 ].
-  Undo.
-  Fail exact (dirprodpair c c0).
-  (* Toplevel input, characters 39-40:
-Error:
-In environment
-X : UU
-R : hrel X
-Y : hSet
-f : X -> X -> Y
-is : iscomprelfun2 R f
-c : setquot R
-c0 : setquot R
-RR := hreldirprod R R : hrel (dirprod X X)
-The term "c" has type "setquot R" while it is expected to have type
-"?42" (unable to find a well-typed instantiation for
-"?42": cannot unify"Type" and "UU").
- *)
diff --git a/test-suite/bugs/opened/3375.v b/test-suite/bugs/opened/3375.v
deleted file mode 100644
index 9cb43413b3..0000000000
--- a/test-suite/bugs/opened/3375.v
+++ /dev/null
@@ -1,48 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *)
-(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then 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 330 lines to 45 lines *)
-
-Set Universe Polymorphism.
-Axiom admit : forall {T}, T.
-Definition UU := Set.
-Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) .
-Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) .
-Definition hProp := sigT (fun X : Type => admit).
-Axiom hProppair : forall ( X : UU ) ( is : admit ), hProp@{Set i}.
-Definition hProptoType := @projT1 _ _ : hProp -> Type .
-Coercion hProptoType: hProp >-> Sortclass.
-Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ).
-Definition ishinh ( X : UU ) : hProp := hProppair ( ishinh_UU X ) admit.
-Definition hsubtypes ( X : UU ) : Type := X -> hProp.
-Axiom carrier : forall { X : UU } ( A : hsubtypes X ), Type.
-Definition hrel ( X : UU ) : Type := X -> X -> hProp.
-Set Printing Universes.
-Definition iseqclass { X : UU } ( R : hrel X ) ( A : hsubtypes X ) : Type.
-  intros; exact ( dirprod ( ishinh ( carrier A ) ) ( dirprod ( forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 )
-                                                             ( forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) )) .
-Defined.
-Definition iseqclassconstr' { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) )
-           ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) : iseqclass R A.
-  intros.
-  apply dirprodpair. { exact ax0. }
-                     apply dirprodpair. { exact ax1. } {exact ax2. }
-Defined.
-Definition iseqclassconstr { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) )
-           ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) : iseqclass R A.
-  pose @iseqclassconstr'.
-  intros.
-  exact (dirprodpair ax0 (dirprodpair ax1 ax2)).
-Fail Defined.
-(* Toplevel input, characters 15-23:
-Error: Illegal application:
-The term "dirprodpair" of type
- "forall (X Y : UU) (x : X), (fun _ : X => Y) x -> {_ : X & Y}"
-cannot be applied to the terms
- "forall x1 x2 : X, R x1 x2 -> A x1 -> A x2"
-   : "Type@{max(Set, Top.476, Top.479)}"
- "forall x1 x2 : X, A x1 -> A x2 -> R x1 x2"
-   : "Type@{max(Set, Top.476, Top.479)}"
- "ax1" : "forall x1 x2 : X, R x1 x2 -> A x1 -> A x2"
- "ax2" : "forall x1 x2 : X, A x1 -> A x2 -> R x1 x2"
-The 1st term has type "Type@{max(Set, Top.476, Top.479)}"
-which should be coercible to "UU".
- *)