From d17d4aa655bfb0160da3cbb73ed056f4fc040bfb Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 4 Sep 2023 15:33:21 +0100 Subject: [PATCH] add universe annotations to Localization.v Signed-off-by: Ali Caglayan --- contrib/dune | 1 - dune | 8 ++++++++ theories/Modalities/Localization.v | 10 +++++----- 3 files changed, 13 insertions(+), 6 deletions(-) diff --git a/contrib/dune b/contrib/dune index 9d5259333e0..366015ace21 100644 --- a/contrib/dune +++ b/contrib/dune @@ -3,4 +3,3 @@ (package coq-hott) (flags -noinit -indices-matter -color on) (theories HoTT)) - diff --git a/dune b/dune index 1e5e68e0ce5..f34c887f5d6 100644 --- a/dune +++ b/dune @@ -38,3 +38,11 @@ HoTT.Tests %{deps} -o))) + +; We modify the default alias to avoid test/ + +(alias + (name default) + (deps + (alias_rec contrib/all) + (alias_rec theories/all))) diff --git a/theories/Modalities/Localization.v b/theories/Modalities/Localization.v index e0892fc4ca4..0c3216fec9b 100644 --- a/theories/Modalities/Localization.v +++ b/theories/Modalities/Localization.v @@ -45,7 +45,7 @@ Then, however, we have to express the hypotheses of the induction principle. We (** ** Dependent extendability *) -Fixpoint ExtendableAlong_Over@{a b c d m} +Fixpoint ExtendableAlong_Over@{a b c d m | a <= m, b <= m, c <= m, d <= m} (n : nat) {A : Type@{a}} {B : Type@{b}} (f : A -> B) (C : B -> Type@{c}) (D : forall b, C b -> Type@{d}) @@ -152,10 +152,10 @@ Proof. Defined. (** Here's the [oo]-version. *) -Definition ooExtendableAlong_Over - {A B : Type} (f : A -> B) (C : B -> Type) - (D : forall b, C b -> Type) (ext : ooExtendableAlong f C) - := forall n, ExtendableAlong_Over n f C D (ext n). +Definition ooExtendableAlong_Over@{a b c d m | a <= m, b <= m, c <= m, d <= m} + {A : Type@{a}} {B : Type@{b}} (f : A -> B) (C : B -> Type@{c}) + (D : forall b, C b -> Type@{d}) (ext : ooExtendableAlong f C) + := forall n, ExtendableAlong_Over@{a b c d m} n f C D (ext n). (** The [oo]-version for trivial dependency. *) Definition ooextendable_over_const