diff options
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r-- | test-suite/bugs/closed/3446.v | 44 | ||||
-rw-r--r-- | test-suite/bugs/closed/3922.v | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/4089.v | 2 |
3 files changed, 26 insertions, 22 deletions
diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v index 4f29b76c6..dce73e1a5 100644 --- a/test-suite/bugs/closed/3446.v +++ b/test-suite/bugs/closed/3446.v @@ -1,28 +1,32 @@ (* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *) -(* Set Asymmetric Patterns. *) -(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *) -(* Notation "A -> B" := (forall (_ : A), B). *) +Module First. +Set Asymmetric Patterns. +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Notation "A -> B" := (forall (_ : A), B). +Set Universe Polymorphism. + -(* Notation "x → y" := (x -> y) *) -(* (at level 99, y at level 200, right associativity): type_scope. *) -(* Record sigT A (P : A -> Type) := *) -(* { projT1 : A ; projT2 : P projT1 }. *) -(* Arguments projT1 {A P} s. *) -(* Arguments projT2 {A P} s. *) -(* Set Universe Polymorphism. *) -(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *) -(* Reserved Notation "x = y" (at level 70, no associativity). *) -(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *) -(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *) -(* Reserved Notation "{ x : A & P }" (at level 0, x at level 99). *) -(* Notation "{ x : A & P }" := (sigT A (fun x => P)) : type_scope. *) +Notation "x → y" := (x -> y) + (at level 99, y at level 200, right associativity): type_scope. +Record sigT A (P : A -> Type) := + { projT1 : A ; projT2 : P projT1 }. +Arguments projT1 {A P} s. +Arguments projT2 {A P} s. +Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). +Reserved Notation "x = y" (at level 70, no associativity). +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). +Notation " x = y " := (paths x y) : type_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. +Reserved Notation "{ x : A & P }" (at level 0, x at level 99). +Notation "{ x : A & P }" := (sigT A (fun x => P)) : type_scope. -(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v & transport _ p (projT2 u) = projT2 v}), u = v. *) -(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *) +Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v & transport _ p (projT2 u) = projT2 v}), u = v. +Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). -(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *) -(* @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *) +Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := + @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). +End First. Set Asymmetric Patterns. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 932084891..0ccc92067 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -43,7 +43,7 @@ Notation IsHProp := (IsTrunc -1). Monomorphic Axiom dummy_funext_type : Type0. Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Record TruncType (n : trunc_index) := BuildTruncType { diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index 1449f242b..c6cb9c35e 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -163,7 +163,7 @@ Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope. Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope. -Inductive Unit : Type1 := +Inductive Unit : Set := tt : Unit. Ltac done := |