diff options
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/4527.v | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4533.v | 11 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4544.v | 3 |
3 files changed, 14 insertions, 8 deletions
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 117d6523a8..f8cedfff6e 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -23,7 +23,9 @@ Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. +Notation two := (S (S O)). Record prod (A B : Type) := pair { fst : A ; snd : B }. @@ -159,7 +161,7 @@ End Adjointify. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -220,12 +222,12 @@ Section ORecursion. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) : O_indpaths g h p (to O P x) = p x - := (fst (snd (extendable_to_O O 2) g h) p).2 x. + := (fst (snd (extendable_to_O O two) g h) p).2 x. End ORecursion. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index c3e0da1117..fd2380a070 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope. Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. + Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. + Notation one := (S O). + Notation two := (S one). Record prod (A B : Type) := pair { fst : A ; snd : B }. Notation "x * y" := (prod x y) : type_scope. Delimit Scope nat_scope with nat. @@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l} (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). Definition O_rec {P Q : Type} {Q_inO : In O Q} (f : P -> Q) : O P -> Q - := (fst (extendable_to_O O 1%nat) f).1. + := (fst (extendable_to_O O one) f).1. Definition O_rec_beta {P Q : Type} {Q_inO : In O Q} (f : P -> Q) (x : P) : O_rec f (to O P x) = f x - := (fst (extendable_to_O O 1%nat) f).2 x. + := (fst (extendable_to_O O one) f).2 x. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. End ORecursion. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 4ad53bc629..13c47edc8f 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. Notation "x + y" := (sum x y) : type_scope. @@ -449,7 +450,7 @@ Section Extensions. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), |