From 1d294be4219cfc3d6cdacc06753096ec9ffa448d Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 17 Jan 2021 17:28:51 +0100 Subject: [PATCH 1/9] bump submodule to 8.13 --- coq-HoTT | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-HoTT b/coq-HoTT index afc828b3e20..5f99fa0c23b 160000 --- a/coq-HoTT +++ b/coq-HoTT @@ -1 +1 @@ -Subproject commit afc828b3e207dd39c59d1501d570a88b2012fd2c +Subproject commit 5f99fa0c23b54ca42b7d5b1e8974cb25280bda07 From 24c9c21d5ed72edb75b4f66f4bffdf364869882a Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 17 Jan 2021 17:30:01 +0100 Subject: [PATCH 2/9] bump coq-scripts submodule --- etc/coq-scripts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/etc/coq-scripts b/etc/coq-scripts index d0b8e808e03..66f4089305e 160000 --- a/etc/coq-scripts +++ b/etc/coq-scripts @@ -1 +1 @@ -Subproject commit d0b8e808e0382d791eb6c0a2d9d751300a2d2057 +Subproject commit 66f4089305e8c6d85eca7a6ff2b8e6c131611fab From e72a712c1d7964f9674974e73de053d661fa0223 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 17 Jan 2021 17:32:15 +0100 Subject: [PATCH 3/9] update INSTALL.md to 8.13 --- INSTALL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/INSTALL.md b/INSTALL.md index 364f7b85f40..2ddcbf1d71d 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -126,7 +126,7 @@ installing ocaml using opam instead, as described above. If you don't want to compile your own copy of Coq, then the HoTT library is compatible with [Coq -8.12](https://github.com/coq/coq/releases/tag/V8.12.0), so you can +8.13](https://github.com/coq/coq/releases/tag/V8.13.0), so you can also install a binary Coq package using a package manager or opam. Paths still need to be set manually. On Debian/Ubuntu, you can also install the master development branch of Coq as your only version of From 95bce7ca1c754511a87c6e8fd4e6041a41bd77f7 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 19 Jan 2021 15:47:35 +0100 Subject: [PATCH 4/9] Adapt library to new hint behaviour --- coq/theories/Init/Datatypes.v | 4 +-- coq/theories/Init/Logic.v | 5 ++-- coq/theories/Init/Logic_Type.v | 2 +- coq/theories/Init/Peano.v | 30 +++++++++---------- coq/theories/Init/Specif.v | 6 ++-- coq/theories/Init/Tactics.v | 2 +- theories/Algebra/Groups/ShortExactSequence.v | 2 -- theories/Basics/Equivalences.v | 1 + theories/Basics/Overture.v | 10 +++++++ theories/Basics/PathGroupoids.v | 1 + theories/Basics/Trunc.v | 3 ++ .../Adjoint/Composition/AssociativityLaw.v | 1 + .../Adjoint/Composition/IdentityLaws.v | 1 + theories/Categories/Category/Core.v | 1 + theories/Categories/Category/Morphisms.v | 7 +++++ theories/Categories/Comma/Core.v | 2 ++ .../Categories/Functor/Composition/Laws.v | 2 ++ theories/Categories/Functor/Core.v | 1 + .../Categories/FunctorCategory/Morphisms.v | 3 ++ theories/Categories/NatCategory.v | 1 + .../Categories/NaturalTransformation/Core.v | 1 + .../PseudonaturalTransformation/Core.v | 1 + theories/Categories/Structure/Core.v | 1 + theories/Classes/implementations/pointwise.v | 8 +++++ .../Classes/interfaces/abstract_algebra.v | 6 ++++ theories/Classes/interfaces/canonical_names.v | 8 +++++ theories/Classes/interfaces/orders.v | 4 +++ theories/Classes/orders/dec_fields.v | 2 ++ theories/Classes/orders/maps.v | 3 ++ theories/Classes/orders/naturals.v | 1 + theories/Classes/orders/orders.v | 6 ++++ theories/Classes/orders/semirings.v | 15 ++++++++++ theories/Classes/theory/apartness.v | 1 + theories/Classes/theory/dec_fields.v | 1 + theories/Classes/theory/fields.v | 2 ++ theories/Classes/theory/groups.v | 6 ++++ theories/Classes/theory/lattices.v | 8 +++++ theories/Classes/theory/naturals.v | 2 ++ theories/Classes/theory/rings.v | 5 ++++ theories/Homotopy/HSpace.v | 18 +++++------ theories/Modalities/Modality.v | 1 + theories/Modalities/ReflectiveSubuniverse.v | 7 +++++ theories/Spaces/BAut/Rigid.v | 3 +- theories/Spaces/Finite.v | 1 + theories/Truncations/Connectedness.v | 4 +-- theories/Truncations/Core.v | 2 ++ theories/Types/Equiv.v | 5 ++++ theories/Types/Sigma.v | 2 ++ theories/WildCat/Type.v | 1 + 49 files changed, 169 insertions(+), 41 deletions(-) diff --git a/coq/theories/Init/Datatypes.v b/coq/theories/Init/Datatypes.v index a6b6bc492b4..b3280ddb495 100644 --- a/coq/theories/Init/Datatypes.v +++ b/coq/theories/Init/Datatypes.v @@ -68,7 +68,7 @@ Notation "A /\ B" := (prod A B) (only parsing) : type_scope. Notation and := prod (only parsing). Notation conj := pair (only parsing). -Hint Resolve pair inl inr : core. +#[global] Hint Resolve pair inl inr : core. Definition prod_curry (A B C : Type) (f : A -> B -> C) (p : prod A B) : C := f (fst p) (snd p). @@ -107,7 +107,7 @@ Inductive identity (A : Type) (a : A) : A -> Type := Scheme identity_rect := Induction for identity Sort Type. -Hint Resolve identity_refl: core. +#[global] Hint Resolve identity_refl: core. Arguments identity {A} _ _. Arguments identity_refl {A a} , [A] a. diff --git a/coq/theories/Init/Logic.v b/coq/theories/Init/Logic.v index 9b51ccb2807..066300f3c6d 100644 --- a/coq/theories/Init/Logic.v +++ b/coq/theories/Init/Logic.v @@ -33,6 +33,5 @@ Definition not (A:Type) : Type := A -> False. (* Notation "~ x" := (not x) : type_scope. *) -Hint Unfold not: core. - -Hint Resolve I : core. +#[global] Hint Unfold not : core. +#[global] Hint Resolve I : core. diff --git a/coq/theories/Init/Logic_Type.v b/coq/theories/Init/Logic_Type.v index b0230c4e906..f02cfbd5ff2 100644 --- a/coq/theories/Init/Logic_Type.v +++ b/coq/theories/Init/Logic_Type.v @@ -75,4 +75,4 @@ Definition identity_rect_r : intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. -Hint Immediate identity_sym not_identity_sym: core v62. +#[global] Hint Immediate identity_sym not_identity_sym: core v62. diff --git a/coq/theories/Init/Peano.v b/coq/theories/Init/Peano.v index df0ceb0fde0..316e4a1b527 100644 --- a/coq/theories/Init/Peano.v +++ b/coq/theories/Init/Peano.v @@ -36,8 +36,8 @@ Definition eq_S := f_equal S. Local Definition f_equal_S := f_equal S. Local Definition f_equal_nat := f_equal (A:=nat). -Hint Resolve f_equal_S : v62. -Hint Resolve f_equal_nat : core. +#[global] Hint Resolve f_equal_S : v62. +#[global] Hint Resolve f_equal_nat : core. (** The predecessor function *) @@ -55,13 +55,13 @@ Qed. (** Injectivity of successor *) Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H. -Hint Immediate eq_add_S: core. +#[global] Hint Immediate eq_add_S: core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. red; auto. Qed. -Hint Resolve not_eq_S: core. +#[global] Hint Resolve not_eq_S: core. Definition IsSucc (n:nat) : Type := match n with @@ -97,14 +97,14 @@ where "n + m" := (plus n m) : nat_scope. Local Definition f_equal2_plus := f_equal2 plus. Local Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). -Hint Resolve f_equal2_plus : v62. -Hint Resolve f_equal2_nat : core. +#[global] Hint Resolve f_equal2_plus : v62. +#[global] Hint Resolve f_equal2_nat : core. Lemma plus_n_O : forall n:nat, n = n + 0. Proof. induction n; simpl; auto. Qed. -Hint Resolve plus_n_O: core. +#[global] Hint Resolve plus_n_O: core. Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. @@ -115,7 +115,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. intros n m; induction n; simpl; auto. Qed. -Hint Resolve plus_n_Sm: core. +#[global] Hint Resolve plus_n_Sm: core. Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). Proof. @@ -138,13 +138,13 @@ Fixpoint mult (n m:nat) : nat := where "n * m" := (mult n m) : nat_scope. Local Definition f_equal2_mult := f_equal2 mult. -Hint Resolve f_equal2_mult : core. +#[global] Hint Resolve f_equal2_mult : core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. induction n; simpl; auto. Qed. -Hint Resolve mult_n_O: core. +#[global] Hint Resolve mult_n_O: core. Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. Proof. @@ -152,7 +152,7 @@ Proof. destruct H; rewrite <- plus_n_Sm; apply eq_S. pattern m at 1 3; elim m; simpl; auto. Qed. -Hint Resolve mult_n_Sm: core. +#[global] Hint Resolve mult_n_Sm: core. (** Standard associated names *) @@ -178,21 +178,21 @@ Inductive le (n:nat) : nat -> Type := | le_S : forall m:nat, le n m -> le n (S m). Local Notation "n <= m" := (le n m) : nat_scope. -Hint Constructors le: core. +#[global] Hint Constructors le: core. (*i equivalent to : "Hints Resolve le_n le_S : core." i*) Definition lt (n m:nat) := S n <= m. -Hint Unfold lt: core. +#[global] Hint Unfold lt: core. Local Infix "<" := lt : nat_scope. Definition ge (n m:nat) := m <= n. -Hint Unfold ge: core. +#[global] Hint Unfold ge: core. Local Infix ">=" := ge : nat_scope. Definition gt (n m:nat) := m < n. -Hint Unfold gt: core. +#[global] Hint Unfold gt: core. Local Infix ">" := gt : nat_scope. diff --git a/coq/theories/Init/Specif.v b/coq/theories/Init/Specif.v index 1a03e6a07b6..fa521a71795 100644 --- a/coq/theories/Init/Specif.v +++ b/coq/theories/Init/Specif.v @@ -70,9 +70,9 @@ Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..)) : type_scope. Notation "'exists2' x , p & q" := (sigT2 (fun x => p) (fun x => q)) - (at level 200, x ident, p at level 200, right associativity) : type_scope. + (at level 200, x name, p at level 200, right associativity) : type_scope. Notation "'exists2' x : t , p & q" := (sigT2 (fun x:t => p) (fun x:t => q)) - (at level 200, x ident, t at level 200, p at level 200, right associativity, + (at level 200, x name, t at level 200, p at level 200, right associativity, format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'") : type_scope. @@ -177,4 +177,4 @@ Proof. apply (h2 h1). Defined. -Hint Resolve existT existT2: core. +#[global] Hint Resolve existT existT2: core. diff --git a/coq/theories/Init/Tactics.v b/coq/theories/Init/Tactics.v index 8b31c780aa9..79cfcecfd2c 100644 --- a/coq/theories/Init/Tactics.v +++ b/coq/theories/Init/Tactics.v @@ -34,5 +34,5 @@ Ltac easy := Tactic Notation "now" tactic(t) := t; easy. Create HintDb rewrite discriminated. -Hint Variables Opaque : rewrite. +#[global] Hint Variables Opaque : rewrite. Create HintDb typeclass_instances discriminated. diff --git a/theories/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v index d86e2d9479f..6d90bf95d3c 100644 --- a/theories/Algebra/Groups/ShortExactSequence.v +++ b/theories/Algebra/Groups/ShortExactSequence.v @@ -40,8 +40,6 @@ Proof. + rapply (transport IsHProp (x:= grp_trivial)). apply path_universe_uncurried. rapply Build_Equiv. - apply isequiv_contr_map. - exact conn. - intro isemb_f. exists (grp_iscomplex_trivial f). intros y; rapply contr_inhabited_hprop. diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v index b8a5fd47ebb..cfe0c7d0ab9 100644 --- a/theories/Basics/Equivalences.v +++ b/theories/Basics/Equivalences.v @@ -386,6 +386,7 @@ Section EquivInverse. End EquivInverse. (** If the goal is [IsEquiv _^-1], then use [isequiv_inverse]; otherwise, don't pretend worry about if the goal is an evar and we want to add a [^-1]. *) +#[global] Hint Extern 0 (IsEquiv _^-1) => apply @isequiv_inverse : typeclass_instances. (** [Equiv A B] is a symmetric relation. *) diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 86b235bb98a..84c1402cc68 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -207,6 +207,7 @@ Definition composeD {A B C} (g : forall b, C b) (f : A -> B) := fun x : A => g ( Global Arguments composeD {A B C}%type_scope (g f)%function_scope x. +#[global] Hint Unfold composeD : core. Notation "g 'oD' f" := (composeD g f) : function_scope. @@ -404,6 +405,7 @@ Global Arguments reflexive_pointwise_paths /. Global Arguments transitive_pointwise_paths /. Global Arguments symmetric_pointwise_paths /. +#[global] Hint Unfold pointwise_paths : typeclass_instances. Notation "f == g" := (pointwise_paths f g) : type_scope. @@ -586,11 +588,14 @@ Global Instance istrunc_paths (A : Type) n `{H : IsTrunc n.+1 A} (x y : A) Existing Class IsTrunc_internal. +#[global] Hint Extern 0 (IsTrunc_internal _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *) +#[global] Hint Extern 0 (IsTrunc _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *) (** Picking up the [forall x y, IsTrunc n (x = y)] instances in the hypotheses is much tricker. We could do something evil where we declare an empty typeclass like [IsTruncSimplification] and use the typeclass as a proxy for allowing typeclass machinery to factor nested [forall]s into the [IsTrunc] via backward reasoning on the type of the hypothesis... but, that's rather complicated, so we instead explicitly list out a few common cases. It should be clear how to extend the pattern. *) +#[global] Hint Extern 10 => progress match goal with | [ H : forall x y : ?T, IsTrunc ?n (x = y) |- _ ] @@ -609,6 +614,7 @@ Notation Contr := (IsTrunc minus_two). Notation IsHProp := (IsTrunc minus_two.+1). Notation IsHSet := (IsTrunc minus_two.+2). +#[global] Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances. (** *** Simple induction *) @@ -657,7 +663,9 @@ Global Arguments path_forall {_ A%type_scope P} (f g)%function_scope _. The hints in [path_hints] are designed to push concatenation *outwards*, eliminate identities and inverses, and associate to the left as far as possible. *) (** TODO: think more carefully about this. Perhaps associating to the right would be more convenient? *) +#[global] Hint Resolve idpath inverse : path_hints. +#[global] Hint Resolve idpath : core. Ltac path_via mid := @@ -674,6 +682,7 @@ Definition Empty_rect := Empty_ind. Definition not (A:Type) : Type := A -> Empty. Notation "~ x" := (not x) : type_scope. Notation "~~ x" := (~ ~x) : type_scope. +#[global] Hint Unfold not: core. Notation "x <> y :> T" := (not (x = y :> T)) : type_scope. Notation "x <> y" := (x <> y :> _) : type_scope. @@ -700,6 +709,7 @@ Scheme Unit_rec := Minimality for Unit Sort Type. Definition Unit_rect := Unit_ind. (** A [Unit] goal should be resolved by [auto] and [trivial]. *) +#[global] Hint Resolve tt : core. Register Unit as core.IDProp.type. diff --git a/theories/Basics/PathGroupoids.v b/theories/Basics/PathGroupoids.v index ab601984e07..d7bef15e58f 100644 --- a/theories/Basics/PathGroupoids.v +++ b/theories/Basics/PathGroupoids.v @@ -1288,6 +1288,7 @@ Defined. (** [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. Given as a notation not a definition so that the resultant terms are literally instances of [concat], with no unfolding required. *) Notation concatR := (fun p q => concat q p). +#[global] Hint Resolve concat_1p concat_p1 concat_p_pp inv_pp inv_V diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v index a0d9a0aa0a1..eb14395bbe1 100644 --- a/theories/Basics/Trunc.v +++ b/theories/Basics/Trunc.v @@ -283,8 +283,11 @@ Definition trunc_hset {n} {A} `{IsHSet A} := (@trunc_leq 0 n.+3 tt _ _). (** Consider the preceding definitions as instances for typeclass search, but only if the requisite hypothesis is already a known assumption; otherwise they result in long or interminable searches. *) +#[global] Hint Immediate trunc_contr : typeclass_instances. +#[global] Hint Immediate trunc_hprop : typeclass_instances. +#[global] Hint Immediate trunc_hset : typeclass_instances. (** Equivalence preserves truncation (this is, of course, trivial with univalence). diff --git a/theories/Categories/Adjoint/Composition/AssociativityLaw.v b/theories/Categories/Adjoint/Composition/AssociativityLaw.v index 88ac021375b..fa422d24935 100644 --- a/theories/Categories/Adjoint/Composition/AssociativityLaw.v +++ b/theories/Categories/Adjoint/Composition/AssociativityLaw.v @@ -47,4 +47,5 @@ Section composition_lemmas. Qed. End composition_lemmas. +#[global] Hint Resolve associativity : category. diff --git a/theories/Categories/Adjoint/Composition/IdentityLaws.v b/theories/Categories/Adjoint/Composition/IdentityLaws.v index f97ae637f91..3e588bfa024 100644 --- a/theories/Categories/Adjoint/Composition/IdentityLaws.v +++ b/theories/Categories/Adjoint/Composition/IdentityLaws.v @@ -52,4 +52,5 @@ Section identity_lemmas. End identity_lemmas. Hint Rewrite @left_identity @right_identity : category. +#[global] Hint Immediate left_identity right_identity : category. diff --git a/theories/Categories/Category/Core.v b/theories/Categories/Category/Core.v index 1604bf7a58f..f0eaf97b57f 100644 --- a/theories/Categories/Category/Core.v +++ b/theories/Categories/Category/Core.v @@ -113,6 +113,7 @@ Create HintDb category discriminated. (** create a hint db for morphisms in categories *) Create HintDb morphism discriminated. +#[global] Hint Resolve left_identity right_identity associativity : category morphism. Hint Rewrite left_identity right_identity : category. Hint Rewrite left_identity right_identity : morphism. diff --git a/theories/Categories/Category/Morphisms.v b/theories/Categories/Category/Morphisms.v index 783c042feb8..c69cd73a94f 100644 --- a/theories/Categories/Category/Morphisms.v +++ b/theories/Categories/Category/Morphisms.v @@ -22,6 +22,7 @@ Arguments morphism_inverse {C s d} m {_}. Local Notation "m ^-1" := (morphism_inverse m) : morphism_scope. +#[global] Hint Resolve left_inverse right_inverse : category morphism. Hint Rewrite @left_inverse @right_inverse : category. Hint Rewrite @left_inverse @right_inverse : morphism. @@ -193,6 +194,7 @@ Section iso_equiv_relation. | abstract iso_comp_t @right_inverse ]. Defined. + #[local] Hint Immediate isisomorphism_inverse : typeclass_instances. (** *** Being isomorphic is a reflexive relation *) @@ -214,6 +216,7 @@ Section iso_equiv_relation. end. End iso_equiv_relation. +#[global] Hint Immediate isisomorphism_inverse : typeclass_instances. (** ** Epimorphisms and Monomorphisms *) @@ -374,6 +377,9 @@ Section EpiMono. End iso. End EpiMono. +#[global] Hint Immediate isisomorphism_inverse : typeclass_instances. + +#[global] Hint Immediate isepimorphism_identity ismonomorphism_identity ismonomorphism_compose isepimorphism_compose @@ -458,6 +464,7 @@ Section iso_lemmas. Defined. End iso_lemmas. +#[global] Hint Extern 1 (@IsIsomorphism _ _ _ (@morphism_of ?C ?D ?F ?s ?d ?m)) => apply (@iso_functor C D F s d m) : typeclass_instances. diff --git a/theories/Categories/Comma/Core.v b/theories/Categories/Comma/Core.v index 214a3795131..557a0a8ae2e 100644 --- a/theories/Categories/Comma/Core.v +++ b/theories/Categories/Comma/Core.v @@ -297,7 +297,9 @@ Qed. End category. *) +#[global] Hint Unfold compose identity : category. +#[global] Hint Constructors morphism object : category. (** ** (co)slice category [(a / F)], [(F / a)] *) diff --git a/theories/Categories/Functor/Composition/Laws.v b/theories/Categories/Functor/Composition/Laws.v index 5f50f103d1a..d06d5b89d2f 100644 --- a/theories/Categories/Functor/Composition/Laws.v +++ b/theories/Categories/Functor/Composition/Laws.v @@ -42,6 +42,7 @@ End identity_lemmas. Hint Rewrite @left_identity @right_identity : category. Hint Rewrite @left_identity @right_identity : functor. +#[global] Hint Immediate left_identity right_identity : category functor. Section composition_lemmas. @@ -65,6 +66,7 @@ Section composition_lemmas. := @path_functor_uncurried_fst _ _ _ ((H o G) o F) (H o (G o F)) 1%path 1%path. End composition_lemmas. +#[global] Hint Resolve associativity : category functor. Section coherence. diff --git a/theories/Categories/Functor/Core.v b/theories/Categories/Functor/Core.v index d3382204c7c..947dc560cde 100644 --- a/theories/Categories/Functor/Core.v +++ b/theories/Categories/Functor/Core.v @@ -60,6 +60,7 @@ Module Export FunctorCoreNotations. Notation "F '_1' m" := (morphism_of F m) : morphism_scope. End FunctorCoreNotations. +#[global] Hint Resolve composition_of identity_of : category functor. Hint Rewrite identity_of : category. Hint Rewrite identity_of : functor. diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v index 917537f457d..ae39b259e96 100644 --- a/theories/Categories/FunctorCategory/Morphisms.v +++ b/theories/Categories/FunctorCategory/Morphisms.v @@ -37,8 +37,10 @@ Proof. - exact (apD10 (ap components_of right_inverse) x). Defined. +#[global] Hint Immediate isisomorphism_components_of : typeclass_instances. (** When one of the functors is the identity functor, we fail to match correctly, because [apply] is stupid. So we do its work for it. *) +#[global] Hint Extern 10 (@IsIsomorphism _ _ _ (@components_of ?C ?D ?F ?G ?T ?x)) => apply (fun H' => @isisomorphism_components_of _ C D F G T H' x) : typeclass_instances. @@ -71,6 +73,7 @@ Proof. ). Defined. +#[global] Hint Immediate isisomorphism_natural_transformation : typeclass_instances. (** ** Variant of [idtoiso] for natural transformations *) diff --git a/theories/Categories/NatCategory.v b/theories/Categories/NatCategory.v index 5326b543b98..73aa46610bf 100644 --- a/theories/Categories/NatCategory.v +++ b/theories/Categories/NatCategory.v @@ -54,6 +54,7 @@ Module Export Core. End NatCategoryCoreNotations. Typeclasses Transparent nat_category. + #[global] Hint Unfold nat_category : core. Arguments nat_category / . End Core. diff --git a/theories/Categories/NaturalTransformation/Core.v b/theories/Categories/NaturalTransformation/Core.v index de9f30b94c2..a677d181735 100644 --- a/theories/Categories/NaturalTransformation/Core.v +++ b/theories/Categories/NaturalTransformation/Core.v @@ -64,6 +64,7 @@ Global Arguments components_of {C D}%category {F G}%functor T%natural_transforma Global Arguments commutes {C D F G} !T / _ _ _ : rename. Global Arguments commutes_sym {C D F G} !T / _ _ _ : rename. +#[global] Hint Resolve commutes : category natural_transformation. (** ** Helper lemmas *) diff --git a/theories/Categories/PseudonaturalTransformation/Core.v b/theories/Categories/PseudonaturalTransformation/Core.v index b8f3b4b9610..5432e65c1f2 100644 --- a/theories/Categories/PseudonaturalTransformation/Core.v +++ b/theories/Categories/PseudonaturalTransformation/Core.v @@ -229,4 +229,5 @@ Create HintDb pseuodnatural_transformation discriminated. Arguments p_components_of {_} {X}%category {F G}%pseudofunctor T%pseudonatural_transformation a%object : rename, simpl nomatch. +#[global] Hint Resolve p_commutes_respects_identity p_commutes_respects_composition : category pseudonatural_transformation. diff --git a/theories/Categories/Structure/Core.v b/theories/Categories/Structure/Core.v index 34be1ccdfd5..8ef73800fb9 100644 --- a/theories/Categories/Structure/Core.v +++ b/theories/Categories/Structure/Core.v @@ -106,6 +106,7 @@ Global Existing Instance istrunc_is_structure_homomorphism. Create HintDb structure_homomorphisms discriminated. +#[global] Hint Resolve is_structure_homomorphism_identity is_structure_homomorphism_composition : structure_homomorphisms. (** When [(P, H)] is a notion of structure, for [α β : P x] we define diff --git a/theories/Classes/implementations/pointwise.v b/theories/Classes/implementations/pointwise.v index 08898ad79cc..51e8879fb01 100644 --- a/theories/Classes/implementations/pointwise.v +++ b/theories/Classes/implementations/pointwise.v @@ -26,6 +26,7 @@ Section contents. (** Try to solve some of the lattice obligations automatically *) Create HintDb lattice_hints. + #[local] Hint Resolve associativity absorption @@ -70,3 +71,10 @@ Section contents. repeat split; try apply _; reduce_fun; apply absorption. Defined. End contents. + +#[global] + Hint Resolve + associativity + absorption + commutativity | 1 : lattice_hints. + diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v index 5722807bccb..1280767b1dc 100644 --- a/theories/Classes/interfaces/abstract_algebra.v +++ b/theories/Classes/interfaces/abstract_algebra.v @@ -48,6 +48,7 @@ Section setoid_morphisms. End setoid_morphisms. (* HOTT TODO check if this is ok/useful *) +#[global] Hint Extern 4 (?f _ = ?f _) => eapply (ap f) : core. Section setoid_binary_morphisms. @@ -155,10 +156,13 @@ Section upper_classes. End upper_classes. (* Due to bug #2528 *) +#[global] Hint Extern 4 (PropHolds (1 <> 0)) => eapply @intdom_nontrivial : typeclass_instances. +#[global] Hint Extern 5 (PropHolds (1 ≶ 0)) => eapply @field_nontrivial : typeclass_instances. +#[global] Hint Extern 5 (PropHolds (1 <> 0)) => eapply @decfield_nontrivial : typeclass_instances. @@ -168,6 +172,7 @@ Integers -> IntegralDomain -> Ring and sometimes directly. Making this an instance with a low priority instead of using intdom_ring:> IsRing forces Coq to take the right way *) +#[global] Hint Extern 10 (IsRing _) => apply @intdom_ring : typeclass_instances. Arguments recip_inverse {A Aplus Amult Azero Aone Anegate Aap Arecip IsField} _. @@ -281,6 +286,7 @@ End jections. Global Instance isinj_idmap A : @IsInjective A A idmap := fun x y => idmap. +#[global] Hint Unfold IsInjective : typeclass_instances. Section strong_injective. diff --git a/theories/Classes/interfaces/canonical_names.v b/theories/Classes/interfaces/canonical_names.v index 985fb184a4d..f79ff83f453 100644 --- a/theories/Classes/interfaces/canonical_names.v +++ b/theories/Classes/interfaces/canonical_names.v @@ -48,6 +48,7 @@ Class TrivialApart A {Aap : Apart A} := ; trivial_apart : forall x y, x ≶ y <-> x <> y }. Definition sig_apart `{Apart A} (P: A -> Type) : Apart (sig P) := fun x y => x.1 ≶ y.1. +#[global] Hint Extern 10 (Apart (sig _)) => apply @sig_apart : typeclass_instances. Class Cast A B := cast: A -> B. @@ -91,8 +92,11 @@ Instance join_is_sg_op `{f : Join A} : SgOp A := f. Instance top_is_mon_unit `{s : Top A} : MonUnit A := s. Instance bottom_is_mon_unit `{s : Bottom A} : MonUnit A := s. +#[global] Hint Extern 4 (Apart (ApartZero _)) => apply @sig_apart : typeclass_instances. +#[global] Hint Extern 4 (Apart (NonNeg _)) => apply @sig_apart : typeclass_instances. +#[global] Hint Extern 4 (Apart (Pos _)) => apply @sig_apart : typeclass_instances. (* Notations: *) @@ -182,8 +186,11 @@ Ltac auto_trans := match goal with [ H: ?R ?x ?y, I: ?R ?y ?z |- ?R ?x ?z] => apply (transitivity H I) end. +#[global] Hint Extern 2 (?x ≤ ?y) => reflexivity : core. +#[global] Hint Extern 4 (?x ≤ ?z) => auto_trans : core. +#[global] Hint Extern 4 (?x < ?z) => auto_trans : core. Class Abs A `{Le A} `{Zero A} `{Negate A} @@ -412,6 +419,7 @@ Arguments enumerator_issurj A {_} _. *) Class PropHolds (P : Type) := prop_holds: P. +#[global] Hint Extern 0 (PropHolds _) => assumption : typeclass_instances. Ltac solve_propholds := diff --git a/theories/Classes/interfaces/orders.v b/theories/Classes/interfaces/orders.v index 3a8c1e8536a..99a35c3f17b 100644 --- a/theories/Classes/interfaces/orders.v +++ b/theories/Classes/interfaces/orders.v @@ -110,7 +110,9 @@ Section srorder_maps. ; strict_order_embedding_reflecting :> StrictlyOrderReflecting }. End srorder_maps. +#[global] Hint Extern 4 (?f _ ≤ ?f _) => apply (order_preserving f) : core. +#[global] Hint Extern 4 (?f _ < ?f _) => apply (strictly_order_preserving f) : core. (* @@ -152,8 +154,10 @@ Class FullPseudoSemiRingOrder `{Apart A} `{Plus A} ; full_pseudo_srorder_le_iff_not_lt_flip : forall x y, x ≤ y <-> ~(y < x) }. (* Due to bug #2528 *) +#[global] Hint Extern 7 (PropHolds (0 < _ * _)) => eapply @pos_mult_compat : typeclass_instances. +#[global] Hint Extern 7 (PropHolds (0 ≤ _ * _)) => eapply @nonneg_mult_compat : typeclass_instances. diff --git a/theories/Classes/orders/dec_fields.v b/theories/Classes/orders/dec_fields.v index 5558cddb1bd..fae205607df 100644 --- a/theories/Classes/orders/dec_fields.v +++ b/theories/Classes/orders/dec_fields.v @@ -108,7 +108,9 @@ Qed. End contents. (* Due to bug #2528 *) +#[global] Hint Extern 12 (PropHolds (0 ≤ _)) => eapply @nonneg_dec_recip_compat : typeclass_instances. +#[global] Hint Extern 12 (PropHolds (0 < _)) => eapply @pos_dec_recip_compat : typeclass_instances. diff --git a/theories/Classes/orders/maps.v b/theories/Classes/orders/maps.v index 630762f6746..1a54ed6e640 100644 --- a/theories/Classes/orders/maps.v +++ b/theories/Classes/orders/maps.v @@ -305,10 +305,13 @@ Section composition. OrderEmbedding f -> OrderEmbedding g -> OrderEmbedding (g ∘ f) := {}. End composition. +#[global] Hint Extern 4 (OrderPreserving (_ ∘ _)) => class_apply @compose_order_preserving : typeclass_instances. +#[global] Hint Extern 4 (OrderReflecting (_ ∘ _)) => class_apply @compose_order_reflecting : typeclass_instances. +#[global] Hint Extern 4 (OrderEmbedding (_ ∘ _)) => class_apply @compose_order_embedding : typeclass_instances. diff --git a/theories/Classes/orders/naturals.v b/theories/Classes/orders/naturals.v index 2ef6a6e696d..01e6a77fd97 100644 --- a/theories/Classes/orders/naturals.v +++ b/theories/Classes/orders/naturals.v @@ -92,4 +92,5 @@ Section another_ring. End another_ring. End naturals_order. +#[global] Hint Extern 20 (PropHolds (_ ≤ _)) => eapply @nat_nonneg : typeclass_instances. diff --git a/theories/Classes/orders/orders.v b/theories/Classes/orders/orders.v index 771dda04249..32278bd20cd 100644 --- a/theories/Classes/orders/orders.v +++ b/theories/Classes/orders/orders.v @@ -314,10 +314,13 @@ Section full_partial_order. End full_partial_order. (* Due to bug #2528 *) +#[global] Hint Extern 5 (PropHolds (_ <> _)) => eapply @strict_po_apart_ne : typeclass_instances. +#[global] Hint Extern 10 (PropHolds (_ ≤ _)) => eapply @lt_le : typeclass_instances. +#[global] Hint Extern 20 (Decidable (_ < _)) => eapply @lt_dec_slow : typeclass_instances. @@ -412,11 +415,14 @@ Section full_pseudo_order. Defined. End full_pseudo_order. +#[global] Hint Extern 8 (Decidable (_ < _)) => eapply @lt_dec : typeclass_instances. (* The following instances would be tempting, but turn out to be a bad idea. +#[global] Hint Extern 10 (PropHolds (_ <> _)) => eapply @le_ne : typeclass_instances. +#[global] Hint Extern 10 (PropHolds (_ <> _)) => eapply @le_ne_flip : typeclass_instances. It will then loop like: diff --git a/theories/Classes/orders/semirings.v b/theories/Classes/orders/semirings.v index 5f5e4ed5937..5383b2dc7b9 100644 --- a/theories/Classes/orders/semirings.v +++ b/theories/Classes/orders/semirings.v @@ -182,6 +182,7 @@ Section semiring_order. End semiring_order. (* Due to bug #2528 *) +#[global] Hint Extern 7 (PropHolds (0 ≤ _ + _)) => eapply @nonneg_plus_compat : typeclass_instances. @@ -345,6 +346,7 @@ Section strict_semiring_order. End strict_semiring_order. (* Due to bug #2528 *) +#[global] Hint Extern 7 (PropHolds (0 < _ + _)) => eapply @pos_plus_compat : typeclass_instances. @@ -557,10 +559,15 @@ Section pseudo_semiring_order. Qed. End pseudo_semiring_order. +#[global] Hint Extern 7 (PropHolds (0 < 1)) => eapply @lt_0_1 : typeclass_instances. +#[global] Hint Extern 7 (PropHolds (0 < 2)) => eapply @lt_0_2 : typeclass_instances. +#[global] Hint Extern 7 (PropHolds (0 < 3)) => eapply @lt_0_3 : typeclass_instances. +#[global] Hint Extern 7 (PropHolds (0 < 4)) => eapply @lt_0_4 : typeclass_instances. +#[global] Hint Extern 7 (PropHolds (2 ≶ 0)) => eapply @apart_0_2 : typeclass_instances. Section full_pseudo_semiring_order. @@ -793,9 +800,13 @@ Section full_pseudo_semiring_order. End full_pseudo_semiring_order. (* Due to bug #2528 *) +#[global] Hint Extern 7 (PropHolds (0 ≤ 1)) => eapply @le_0_1 : typeclass_instances. +#[global] Hint Extern 7 (PropHolds (0 ≤ 2)) => eapply @le_0_2 : typeclass_instances. +#[global] Hint Extern 7 (PropHolds (0 ≤ 3)) => eapply @le_0_3 : typeclass_instances. +#[global] Hint Extern 7 (PropHolds (0 ≤ 4)) => eapply @le_0_4 : typeclass_instances. Section dec_semiring_order. @@ -939,13 +950,17 @@ Section another_semiring_strict. End another_semiring_strict. (* Due to bug #2528 *) +#[global] Hint Extern 15 (PropHolds (_ ≤ _ _)) => eapply @preserves_nonneg : typeclass_instances. +#[global] Hint Extern 15 (PropHolds (_ < _ _)) => eapply @preserves_pos : typeclass_instances. (* Oddly enough, the above hints do not work for goals of the following shape? *) +#[global] Hint Extern 15 (PropHolds (_ ≤ '_)) => eapply @preserves_nonneg : typeclass_instances. +#[global] Hint Extern 15 (PropHolds (_ < '_)) => eapply @preserves_pos : typeclass_instances. diff --git a/theories/Classes/theory/apartness.v b/theories/Classes/theory/apartness.v index 787792c4432..31c6a09be30 100644 --- a/theories/Classes/theory/apartness.v +++ b/theories/Classes/theory/apartness.v @@ -23,6 +23,7 @@ Qed. End contents. (* Due to bug #2528 *) +#[global] Hint Extern 3 (PropHolds (_ <> _)) => eapply @apart_ne : typeclass_instances. Lemma projected_strong_setoid `{IsApart B} `{Apart A} `{IsHSet A} diff --git a/theories/Classes/theory/dec_fields.v b/theories/Classes/theory/dec_fields.v index 44408d4c3f2..2575d94f64a 100644 --- a/theories/Classes/theory/dec_fields.v +++ b/theories/Classes/theory/dec_fields.v @@ -177,6 +177,7 @@ Qed. End contents. (* Due to bug #2528 *) +#[global] Hint Extern 7 (PropHolds (/ _ <> 0)) => eapply @dec_recip_ne_0 : typeclass_instances. diff --git a/theories/Classes/theory/fields.v b/theories/Classes/theory/fields.v index 9d5dc145376..33fe87bc4ec 100644 --- a/theories/Classes/theory/fields.v +++ b/theories/Classes/theory/fields.v @@ -272,8 +272,10 @@ Qed. End field_properties. (* Due to bug #2528 *) +#[global] Hint Extern 8 (PropHolds (// _ ≶ 0)) => eapply @recip_apart_zero : typeclass_instances. +#[global] Hint Extern 8 (PropHolds (_ * _ ≶ 0)) => eapply @mult_apart_zero : typeclass_instances. diff --git a/theories/Classes/theory/groups.v b/theories/Classes/theory/groups.v index 9b42044a4bb..000bdd541b4 100644 --- a/theories/Classes/theory/groups.v +++ b/theories/Classes/theory/groups.v @@ -293,17 +293,23 @@ Section compose_mor. End compose_mor. +#[global] Hint Extern 4 (IsSemiGroupPreserving (_ ∘ _)) => class_apply @compose_sg_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsMonoidPreserving (_ ∘ _)) => class_apply @compose_monoid_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsSemiGroupPreserving (_ o _)) => class_apply @compose_sg_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsMonoidPreserving (_ o _)) => class_apply @compose_monoid_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsSemiGroupPreserving (_^-1)) => class_apply @invert_sg_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsMonoidPreserving (_^-1)) => class_apply @invert_monoid_morphism : typeclass_instances. diff --git a/theories/Classes/theory/lattices.v b/theories/Classes/theory/lattices.v index 90432ccc667..13ac5d8e36d 100644 --- a/theories/Classes/theory/lattices.v +++ b/theories/Classes/theory/lattices.v @@ -229,19 +229,27 @@ Section morphism_composition. Qed. End morphism_composition. +#[global] Hint Extern 4 (IsJoinPreserving (_ ∘ _)) => class_apply @compose_join_sl_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsMeetPreserving (_ ∘ _)) => class_apply @compose_meet_sl_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsBoundedJoinPreserving (_ ∘ _)) => class_apply @compose_bounded_join_sl_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsLatticePreserving (_ ∘ _)) => class_apply @compose_lattice_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsJoinPreserving (_^-1)) => class_apply @invert_join_sl_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsMeetPreserving (_^-1)) => class_apply @invert_meet_sl_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsBoundedJoinPreserving (_^-1)) => class_apply @invert_bounded_join_sl_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsLatticePreserving (_^-1)) => class_apply @invert_lattice_morphism : typeclass_instances. diff --git a/theories/Classes/theory/naturals.v b/theories/Classes/theory/naturals.v index c2b4a23c20f..4147082bbd4 100644 --- a/theories/Classes/theory/naturals.v +++ b/theories/Classes/theory/naturals.v @@ -242,7 +242,9 @@ End with_a_ring. End contents. (* Due to bug #2528 *) +#[global] Hint Extern 6 (PropHolds (1 <> 0)) => eapply @nat_nontrivial : typeclass_instances. +#[global] Hint Extern 6 (PropHolds (1 ≶ 0)) => eapply @nat_nontrivial_apart : typeclass_instances. diff --git a/theories/Classes/theory/rings.v b/theories/Classes/theory/rings.v index b6e19f69707..40033e166dc 100644 --- a/theories/Classes/theory/rings.v +++ b/theories/Classes/theory/rings.v @@ -128,6 +128,7 @@ Section semiring_props. End semiring_props. (* Due to bug #2528 *) +#[global] Hint Extern 3 (PropHolds (_ * _ <> 0)) => eapply @mult_ne_0 : typeclass_instances. Section semiringmor_props. @@ -179,6 +180,7 @@ Section semiringmor_props. End semiringmor_props. (* Due to bug #2528 *) +#[global] Hint Extern 12 (PropHolds (_ _ <> 0)) => eapply @isinjective_ne_0 : typeclass_instances. @@ -366,6 +368,7 @@ Section integral_domain_props. End integral_domain_props. (* Due to bug #2528 *) +#[global] Hint Extern 6 (PropHolds (1 ≶ 0)) => eapply @intdom_nontrivial_apart : typeclass_instances. @@ -466,7 +469,9 @@ Section morphism_composition. Qed. End morphism_composition. +#[global] Hint Extern 4 (IsSemiRingPreserving (_ ∘ _)) => class_apply @compose_sr_morphism : typeclass_instances. +#[global] Hint Extern 4 (IsSemiRingPreserving (_^-1)) => class_apply @invert_sr_morphism : typeclass_instances. diff --git a/theories/Homotopy/HSpace.v b/theories/Homotopy/HSpace.v index f110172ca77..a6390126c81 100644 --- a/theories/Homotopy/HSpace.v +++ b/theories/Homotopy/HSpace.v @@ -28,22 +28,20 @@ Section HSpaceProperties. : forall (a : A), IsEquiv (fun x => a * x). Proof. refine (conn_map_elim (-1) (unit_name hspace_id) _ _). - + exact (conn_point_incl hspace_id). - + apply Unit_ind. - srapply (isequiv_homotopic idmap). - intro a; symmetry. - apply left_identity. + apply Unit_ind. + srapply (isequiv_homotopic idmap). + intro a; symmetry. + apply left_identity. Defined. Global Instance isequiv_hspace_right_op : forall (a : A), IsEquiv (fun x => x * a). Proof. refine (conn_map_elim (-1) (unit_name hspace_id) _ _). - + exact (conn_point_incl hspace_id). - + apply Unit_ind. - srapply (isequiv_homotopic idmap). - intro a; symmetry. - apply right_identity. + apply Unit_ind. + srapply (isequiv_homotopic idmap). + intro a; symmetry. + apply right_identity. Defined. Definition equiv_hspace_left_op (a : A) : A <~> A diff --git a/theories/Modalities/Modality.v b/theories/Modalities/Modality.v index 724f06f0492..64815d30265 100644 --- a/theories/Modalities/Modality.v +++ b/theories/Modalities/Modality.v @@ -146,6 +146,7 @@ Defined. Coercion modality_to_reflective_subuniverse : Modality >-> ReflectiveSubuniverse. (** Unfortunately, sometimes [modality_subuniv] pops up anyway. The following hint helps typeclass inference look through it. *) +#[global] Hint Extern 0 (In (modality_subuniv _) _) => progress change modality_subuniv with (rsu_subuniv o modality_to_reflective_subuniverse) in * : typeclass_instances. (** Modalities are precisely the reflective subuniverses that are [<<] themselves. *) diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v index 27243d03e5c..fd0fef64ebf 100644 --- a/theories/Modalities/ReflectiveSubuniverse.v +++ b/theories/Modalities/ReflectiveSubuniverse.v @@ -481,6 +481,7 @@ Section Reflective_Subuniverse. := fun _ => inO_equiv_inO (O T) (to O T)^-1. (* We don't make this an ordinary instance, but we allow it to solve [In O] constraints if we already have [IsEquiv] as a hypothesis. *) + #[local] Hint Immediate inO_isequiv_to_O : typeclass_instances. Definition inO_iff_isequiv_to_O (T:Type) @@ -853,6 +854,7 @@ Section Reflective_Subuniverse. all: refine (inO_hfiber pr1 x); assumption. Defined. + #[local] Hint Immediate inO_unsigma : typeclass_instances. (** The reflector preserving hfibers is a characterization of lex modalities. Here is the comparison map. *) @@ -1704,6 +1706,7 @@ Section ConnectedMaps. (equiv_sigma_contr (fun a:A => const tt a = tt)) _). Defined. + #[local] Hint Immediate isconnected_conn_map_to_unit : typeclass_instances. Global Instance conn_map_to_unit_isconnected {A : Type} @@ -2058,3 +2061,7 @@ Proof. - pose (inO_leq O' (Sep O)); intros; rapply ooextendable_conn_map_inO. Defined. + +#[global] Hint Immediate inO_isequiv_to_O : typeclass_instances. +#[global] Hint Immediate inO_unsigma : typeclass_instances. +#[global] Hint Immediate isconnected_conn_map_to_unit : typeclass_instances. diff --git a/theories/Spaces/BAut/Rigid.v b/theories/Spaces/BAut/Rigid.v index c34298581a4..8c76dd2cdbe 100644 --- a/theories/Spaces/BAut/Rigid.v +++ b/theories/Spaces/BAut/Rigid.v @@ -104,8 +104,7 @@ Proof. assert (MH : forall (a:A) (f:X*A -> X*A) (x:X), fst (f (x,a)) = fst (f (x,a0))). { refine (conn_map_elim (Tr n) (unit_name a0) _ _). - - apply conn_point_incl; assumption. - - intros; reflexivity. } + intros; reflexivity. } assert (MC : forall (f g :X*A -> X*A), M (g o f) == M g o M f). { intros f g x; unfold M. transitivity (fst (g (fst (f (x,a0)), snd (f (x,a0))))). diff --git a/theories/Spaces/Finite.v b/theories/Spaces/Finite.v index 26b824375a7..87c2afd0b49 100644 --- a/theories/Spaces/Finite.v +++ b/theories/Spaces/Finite.v @@ -468,6 +468,7 @@ Proof. - refine (finite_equiv Empty nx^-1 _). Defined. +#[global] Hint Immediate finite_decidable_hprop : typeclass_instances. (** It follows that the propositional truncation of any finite set is finite. *) diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v index 72a0cf1d71a..b9d56ec4c87 100644 --- a/theories/Truncations/Connectedness.v +++ b/theories/Truncations/Connectedness.v @@ -76,12 +76,12 @@ Proof. apply O_lex_leq_Tr. Defined. -Hint Immediate conn_point_incl : typeclass_instances. - (** Note that [OO_cancelR_conn_map] and [OO_cancelL_conn_map] (Proposition 2.31 of CORS) generalize the above statements to 2/3 of a 2-out-of-3 property for connected maps, for any reflective subuniverse and its subuniverse of separated types. If useful, we could specialize that more general form explicitly to truncations. *) End Extensions. +#[global] Hint Immediate conn_point_incl : typeclass_instances. + (** ** Decreasing connectedness *) (** An [n.+1]-connected type is also [n]-connected. This obviously can't be an [Instance]! *) diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v index 88849c956e6..f333dffd724 100644 --- a/theories/Truncations/Core.v +++ b/theories/Truncations/Core.v @@ -137,6 +137,7 @@ Defined. (** Instead, we make the latter an immediate instance, but with high cost (i.e. low priority) so that it doesn't override the ordinary lemmas about truncation. Unfortunately, [Hint Immediate] doesn't allow specifying a cost, so we use [Hint Extern] instead. *) (** Hint Immediate istrunc_inO_tr : typeclass_instances. *) (** See https://github.com/coq/coq/issues/11697 *) +#[global] Hint Extern 1000 (IsTrunc _ _) => simple apply istrunc_inO_tr; solve [ trivial ] : typeclass_instances. (** This doesn't seem to be quite the same as [Hint Immediate] with a different cost either, though; see the comment in the proof of [Trunc_min] below. *) @@ -157,6 +158,7 @@ Proof. assumption. Defined. +#[global] Hint Immediate istruncmap_mapinO_tr : typeclass_instances. (** ** A few special things about the (-1)-truncation. *) diff --git a/theories/Types/Equiv.v b/theories/Types/Equiv.v index ab642a0f818..b3949383f13 100644 --- a/theories/Types/Equiv.v +++ b/theories/Types/Equiv.v @@ -31,6 +31,7 @@ Section AssumeFunext. Defined. (** As usual, we can't make both of these [Instances]. *) + #[local] Hint Immediate isequiv_contr_map : typeclass_instances. (** It follows that when proving a map is an equivalence, we may assume its codomain is inhabited. *) @@ -186,3 +187,7 @@ Section AssumeFunext. Defined. End AssumeFunext. + +(** We make this a global hint outside of the section. *) +#[global] +Hint Immediate isequiv_contr_map : typeclass_instances. diff --git a/theories/Types/Sigma.v b/theories/Types/Sigma.v index 847cc5b1acd..5c3f58b4cf2 100644 --- a/theories/Types/Sigma.v +++ b/theories/Types/Sigma.v @@ -629,6 +629,7 @@ Global Instance isequiv_path_sigma_hprop {A P} `{forall x : A, IsHProp (P x)} {u : IsEquiv (@path_sigma_hprop A P _ u v) | 100 := isequiv_compose. +#[global] Hint Immediate isequiv_path_sigma_hprop : typeclass_instances. Definition equiv_path_sigma_hprop {A : Type} {P : A -> Type} @@ -642,6 +643,7 @@ Definition isequiv_pr1_path_hprop {A} {P : A -> Type} : IsEquiv (@pr1_path A P x y) := _ : IsEquiv (path_sigma_hprop x y)^-1. +#[global] Hint Immediate isequiv_pr1_path_hprop : typeclass_instances. (** We define this for ease of [SearchAbout IsEquiv ap pr1] *) diff --git a/theories/WildCat/Type.v b/theories/WildCat/Type.v index fc57c46120d..4106c8a7deb 100644 --- a/theories/WildCat/Type.v +++ b/theories/WildCat/Type.v @@ -78,6 +78,7 @@ Proof. assumption. Defined. +#[global] Hint Immediate catie_isequiv : typeclass_instances. Global Instance isinitial_zero : IsInitial Empty. From e7b1181f73002d35beb471829d2c82b6d462dfe3 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 19 Jan 2021 16:02:30 +0100 Subject: [PATCH 5/9] adapted to new number notation syntax --- theories/Basics/Trunc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v index eb14395bbe1..874973db824 100644 --- a/theories/Basics/Trunc.v +++ b/theories/Basics/Trunc.v @@ -75,7 +75,7 @@ Definition trunc_index_to_int n := | n => Decimal.Pos (Decimal.rev (trunc_index_to_little_uint n Decimal.zero)) end. -Numeral Notation trunc_index int_to_trunc_index trunc_index_to_int : trunc_scope (warning after 5000). +Number Notation trunc_index int_to_trunc_index trunc_index_to_int : trunc_scope. (** ** Arithmetic on truncation-levels. *) Fixpoint trunc_index_add (m n : trunc_index) : trunc_index From bc0f9d96da9569e11ee6cce433e4974162430f9a Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 19 Jan 2021 17:59:11 +0100 Subject: [PATCH 6/9] replaced #[global] with #[export] --- coq/theories/Init/Datatypes.v | 4 +-- coq/theories/Init/Logic.v | 4 +-- coq/theories/Init/Logic_Type.v | 2 +- coq/theories/Init/Peano.v | 30 +++++++++---------- coq/theories/Init/Specif.v | 2 +- coq/theories/Init/Tactics.v | 2 +- theories/Basics/Equivalences.v | 2 +- theories/Basics/Overture.v | 20 ++++++------- theories/Basics/PathGroupoids.v | 2 +- theories/Basics/Trunc.v | 6 ++-- .../Adjoint/Composition/AssociativityLaw.v | 2 +- .../Adjoint/Composition/IdentityLaws.v | 2 +- theories/Categories/Category/Core.v | 2 +- theories/Categories/Category/Morphisms.v | 10 +++---- theories/Categories/Comma/Core.v | 4 +-- .../Categories/Functor/Composition/Laws.v | 4 +-- theories/Categories/Functor/Core.v | 2 +- .../Categories/FunctorCategory/Morphisms.v | 6 ++-- theories/Categories/NatCategory.v | 2 +- .../Categories/NaturalTransformation/Core.v | 2 +- .../PseudonaturalTransformation/Core.v | 2 +- theories/Categories/Structure/Core.v | 2 +- theories/Classes/implementations/pointwise.v | 2 +- .../Classes/interfaces/abstract_algebra.v | 12 ++++---- theories/Classes/interfaces/canonical_names.v | 16 +++++----- theories/Classes/interfaces/orders.v | 8 ++--- theories/Classes/orders/dec_fields.v | 4 +-- theories/Classes/orders/maps.v | 6 ++-- theories/Classes/orders/naturals.v | 2 +- theories/Classes/orders/orders.v | 12 ++++---- theories/Classes/orders/semirings.v | 30 +++++++++---------- theories/Classes/theory/apartness.v | 2 +- theories/Classes/theory/dec_fields.v | 2 +- theories/Classes/theory/fields.v | 4 +-- theories/Classes/theory/groups.v | 12 ++++---- theories/Classes/theory/lattices.v | 16 +++++----- theories/Classes/theory/naturals.v | 4 +-- theories/Classes/theory/rings.v | 10 +++---- theories/Modalities/Modality.v | 2 +- theories/Modalities/ReflectiveSubuniverse.v | 6 ++-- theories/Spaces/Finite.v | 2 +- theories/Truncations/Connectedness.v | 2 +- theories/Truncations/Core.v | 4 +-- theories/Types/Equiv.v | 2 +- theories/Types/Sigma.v | 4 +-- theories/WildCat/Type.v | 2 +- 46 files changed, 140 insertions(+), 140 deletions(-) diff --git a/coq/theories/Init/Datatypes.v b/coq/theories/Init/Datatypes.v index b3280ddb495..3a69762dca8 100644 --- a/coq/theories/Init/Datatypes.v +++ b/coq/theories/Init/Datatypes.v @@ -68,7 +68,7 @@ Notation "A /\ B" := (prod A B) (only parsing) : type_scope. Notation and := prod (only parsing). Notation conj := pair (only parsing). -#[global] Hint Resolve pair inl inr : core. +#[export] Hint Resolve pair inl inr : core. Definition prod_curry (A B C : Type) (f : A -> B -> C) (p : prod A B) : C := f (fst p) (snd p). @@ -107,7 +107,7 @@ Inductive identity (A : Type) (a : A) : A -> Type := Scheme identity_rect := Induction for identity Sort Type. -#[global] Hint Resolve identity_refl: core. +#[export] Hint Resolve identity_refl: core. Arguments identity {A} _ _. Arguments identity_refl {A a} , [A] a. diff --git a/coq/theories/Init/Logic.v b/coq/theories/Init/Logic.v index 066300f3c6d..55c00ed9a56 100644 --- a/coq/theories/Init/Logic.v +++ b/coq/theories/Init/Logic.v @@ -33,5 +33,5 @@ Definition not (A:Type) : Type := A -> False. (* Notation "~ x" := (not x) : type_scope. *) -#[global] Hint Unfold not : core. -#[global] Hint Resolve I : core. +#[export] Hint Unfold not : core. +#[export] Hint Resolve I : core. diff --git a/coq/theories/Init/Logic_Type.v b/coq/theories/Init/Logic_Type.v index f02cfbd5ff2..30f6cdeb351 100644 --- a/coq/theories/Init/Logic_Type.v +++ b/coq/theories/Init/Logic_Type.v @@ -75,4 +75,4 @@ Definition identity_rect_r : intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. -#[global] Hint Immediate identity_sym not_identity_sym: core v62. +#[export] Hint Immediate identity_sym not_identity_sym: core v62. diff --git a/coq/theories/Init/Peano.v b/coq/theories/Init/Peano.v index 316e4a1b527..8a6604757f7 100644 --- a/coq/theories/Init/Peano.v +++ b/coq/theories/Init/Peano.v @@ -36,8 +36,8 @@ Definition eq_S := f_equal S. Local Definition f_equal_S := f_equal S. Local Definition f_equal_nat := f_equal (A:=nat). -#[global] Hint Resolve f_equal_S : v62. -#[global] Hint Resolve f_equal_nat : core. +#[export] Hint Resolve f_equal_S : v62. +#[export] Hint Resolve f_equal_nat : core. (** The predecessor function *) @@ -55,13 +55,13 @@ Qed. (** Injectivity of successor *) Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H. -#[global] Hint Immediate eq_add_S: core. +#[export] Hint Immediate eq_add_S: core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. red; auto. Qed. -#[global] Hint Resolve not_eq_S: core. +#[export] Hint Resolve not_eq_S: core. Definition IsSucc (n:nat) : Type := match n with @@ -97,14 +97,14 @@ where "n + m" := (plus n m) : nat_scope. Local Definition f_equal2_plus := f_equal2 plus. Local Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). -#[global] Hint Resolve f_equal2_plus : v62. -#[global] Hint Resolve f_equal2_nat : core. +#[export] Hint Resolve f_equal2_plus : v62. +#[export] Hint Resolve f_equal2_nat : core. Lemma plus_n_O : forall n:nat, n = n + 0. Proof. induction n; simpl; auto. Qed. -#[global] Hint Resolve plus_n_O: core. +#[export] Hint Resolve plus_n_O: core. Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. @@ -115,7 +115,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. intros n m; induction n; simpl; auto. Qed. -#[global] Hint Resolve plus_n_Sm: core. +#[export] Hint Resolve plus_n_Sm: core. Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). Proof. @@ -138,13 +138,13 @@ Fixpoint mult (n m:nat) : nat := where "n * m" := (mult n m) : nat_scope. Local Definition f_equal2_mult := f_equal2 mult. -#[global] Hint Resolve f_equal2_mult : core. +#[export] Hint Resolve f_equal2_mult : core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. induction n; simpl; auto. Qed. -#[global] Hint Resolve mult_n_O: core. +#[export] Hint Resolve mult_n_O: core. Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. Proof. @@ -152,7 +152,7 @@ Proof. destruct H; rewrite <- plus_n_Sm; apply eq_S. pattern m at 1 3; elim m; simpl; auto. Qed. -#[global] Hint Resolve mult_n_Sm: core. +#[export] Hint Resolve mult_n_Sm: core. (** Standard associated names *) @@ -178,21 +178,21 @@ Inductive le (n:nat) : nat -> Type := | le_S : forall m:nat, le n m -> le n (S m). Local Notation "n <= m" := (le n m) : nat_scope. -#[global] Hint Constructors le: core. +#[export] Hint Constructors le: core. (*i equivalent to : "Hints Resolve le_n le_S : core." i*) Definition lt (n m:nat) := S n <= m. -#[global] Hint Unfold lt: core. +#[export] Hint Unfold lt: core. Local Infix "<" := lt : nat_scope. Definition ge (n m:nat) := m <= n. -#[global] Hint Unfold ge: core. +#[export] Hint Unfold ge: core. Local Infix ">=" := ge : nat_scope. Definition gt (n m:nat) := m < n. -#[global] Hint Unfold gt: core. +#[export] Hint Unfold gt: core. Local Infix ">" := gt : nat_scope. diff --git a/coq/theories/Init/Specif.v b/coq/theories/Init/Specif.v index fa521a71795..f207e021fdb 100644 --- a/coq/theories/Init/Specif.v +++ b/coq/theories/Init/Specif.v @@ -177,4 +177,4 @@ Proof. apply (h2 h1). Defined. -#[global] Hint Resolve existT existT2: core. +#[export] Hint Resolve existT existT2: core. diff --git a/coq/theories/Init/Tactics.v b/coq/theories/Init/Tactics.v index 79cfcecfd2c..7fa31ce4e88 100644 --- a/coq/theories/Init/Tactics.v +++ b/coq/theories/Init/Tactics.v @@ -34,5 +34,5 @@ Ltac easy := Tactic Notation "now" tactic(t) := t; easy. Create HintDb rewrite discriminated. -#[global] Hint Variables Opaque : rewrite. +#[export] Hint Variables Opaque : rewrite. Create HintDb typeclass_instances discriminated. diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v index cfe0c7d0ab9..1443d5a02e8 100644 --- a/theories/Basics/Equivalences.v +++ b/theories/Basics/Equivalences.v @@ -386,7 +386,7 @@ Section EquivInverse. End EquivInverse. (** If the goal is [IsEquiv _^-1], then use [isequiv_inverse]; otherwise, don't pretend worry about if the goal is an evar and we want to add a [^-1]. *) -#[global] +#[export] Hint Extern 0 (IsEquiv _^-1) => apply @isequiv_inverse : typeclass_instances. (** [Equiv A B] is a symmetric relation. *) diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 84c1402cc68..35b5ac783d5 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -207,7 +207,7 @@ Definition composeD {A B C} (g : forall b, C b) (f : A -> B) := fun x : A => g ( Global Arguments composeD {A B C}%type_scope (g f)%function_scope x. -#[global] +#[export] Hint Unfold composeD : core. Notation "g 'oD' f" := (composeD g f) : function_scope. @@ -405,7 +405,7 @@ Global Arguments reflexive_pointwise_paths /. Global Arguments transitive_pointwise_paths /. Global Arguments symmetric_pointwise_paths /. -#[global] +#[export] Hint Unfold pointwise_paths : typeclass_instances. Notation "f == g" := (pointwise_paths f g) : type_scope. @@ -588,14 +588,14 @@ Global Instance istrunc_paths (A : Type) n `{H : IsTrunc n.+1 A} (x y : A) Existing Class IsTrunc_internal. -#[global] +#[export] Hint Extern 0 (IsTrunc_internal _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *) -#[global] +#[export] Hint Extern 0 (IsTrunc _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *) (** Picking up the [forall x y, IsTrunc n (x = y)] instances in the hypotheses is much tricker. We could do something evil where we declare an empty typeclass like [IsTruncSimplification] and use the typeclass as a proxy for allowing typeclass machinery to factor nested [forall]s into the [IsTrunc] via backward reasoning on the type of the hypothesis... but, that's rather complicated, so we instead explicitly list out a few common cases. It should be clear how to extend the pattern. *) -#[global] +#[export] Hint Extern 10 => progress match goal with | [ H : forall x y : ?T, IsTrunc ?n (x = y) |- _ ] @@ -614,7 +614,7 @@ Notation Contr := (IsTrunc minus_two). Notation IsHProp := (IsTrunc minus_two.+1). Notation IsHSet := (IsTrunc minus_two.+2). -#[global] +#[export] Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances. (** *** Simple induction *) @@ -663,9 +663,9 @@ Global Arguments path_forall {_ A%type_scope P} (f g)%function_scope _. The hints in [path_hints] are designed to push concatenation *outwards*, eliminate identities and inverses, and associate to the left as far as possible. *) (** TODO: think more carefully about this. Perhaps associating to the right would be more convenient? *) -#[global] +#[export] Hint Resolve idpath inverse : path_hints. -#[global] +#[export] Hint Resolve idpath : core. Ltac path_via mid := @@ -682,7 +682,7 @@ Definition Empty_rect := Empty_ind. Definition not (A:Type) : Type := A -> Empty. Notation "~ x" := (not x) : type_scope. Notation "~~ x" := (~ ~x) : type_scope. -#[global] +#[export] Hint Unfold not: core. Notation "x <> y :> T" := (not (x = y :> T)) : type_scope. Notation "x <> y" := (x <> y :> _) : type_scope. @@ -709,7 +709,7 @@ Scheme Unit_rec := Minimality for Unit Sort Type. Definition Unit_rect := Unit_ind. (** A [Unit] goal should be resolved by [auto] and [trivial]. *) -#[global] +#[export] Hint Resolve tt : core. Register Unit as core.IDProp.type. diff --git a/theories/Basics/PathGroupoids.v b/theories/Basics/PathGroupoids.v index d7bef15e58f..89e96a4fe52 100644 --- a/theories/Basics/PathGroupoids.v +++ b/theories/Basics/PathGroupoids.v @@ -1288,7 +1288,7 @@ Defined. (** [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. Given as a notation not a definition so that the resultant terms are literally instances of [concat], with no unfolding required. *) Notation concatR := (fun p q => concat q p). -#[global] +#[export] Hint Resolve concat_1p concat_p1 concat_p_pp inv_pp inv_V diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v index 874973db824..1ff51f7d26f 100644 --- a/theories/Basics/Trunc.v +++ b/theories/Basics/Trunc.v @@ -283,11 +283,11 @@ Definition trunc_hset {n} {A} `{IsHSet A} := (@trunc_leq 0 n.+3 tt _ _). (** Consider the preceding definitions as instances for typeclass search, but only if the requisite hypothesis is already a known assumption; otherwise they result in long or interminable searches. *) -#[global] +#[export] Hint Immediate trunc_contr : typeclass_instances. -#[global] +#[export] Hint Immediate trunc_hprop : typeclass_instances. -#[global] +#[export] Hint Immediate trunc_hset : typeclass_instances. (** Equivalence preserves truncation (this is, of course, trivial with univalence). diff --git a/theories/Categories/Adjoint/Composition/AssociativityLaw.v b/theories/Categories/Adjoint/Composition/AssociativityLaw.v index fa422d24935..b69bb65a305 100644 --- a/theories/Categories/Adjoint/Composition/AssociativityLaw.v +++ b/theories/Categories/Adjoint/Composition/AssociativityLaw.v @@ -47,5 +47,5 @@ Section composition_lemmas. Qed. End composition_lemmas. -#[global] +#[export] Hint Resolve associativity : category. diff --git a/theories/Categories/Adjoint/Composition/IdentityLaws.v b/theories/Categories/Adjoint/Composition/IdentityLaws.v index 3e588bfa024..59c9b26ac5a 100644 --- a/theories/Categories/Adjoint/Composition/IdentityLaws.v +++ b/theories/Categories/Adjoint/Composition/IdentityLaws.v @@ -52,5 +52,5 @@ Section identity_lemmas. End identity_lemmas. Hint Rewrite @left_identity @right_identity : category. -#[global] +#[export] Hint Immediate left_identity right_identity : category. diff --git a/theories/Categories/Category/Core.v b/theories/Categories/Category/Core.v index f0eaf97b57f..82000970906 100644 --- a/theories/Categories/Category/Core.v +++ b/theories/Categories/Category/Core.v @@ -113,7 +113,7 @@ Create HintDb category discriminated. (** create a hint db for morphisms in categories *) Create HintDb morphism discriminated. -#[global] +#[export] Hint Resolve left_identity right_identity associativity : category morphism. Hint Rewrite left_identity right_identity : category. Hint Rewrite left_identity right_identity : morphism. diff --git a/theories/Categories/Category/Morphisms.v b/theories/Categories/Category/Morphisms.v index c69cd73a94f..ca4ff1d802a 100644 --- a/theories/Categories/Category/Morphisms.v +++ b/theories/Categories/Category/Morphisms.v @@ -22,7 +22,7 @@ Arguments morphism_inverse {C s d} m {_}. Local Notation "m ^-1" := (morphism_inverse m) : morphism_scope. -#[global] +#[export] Hint Resolve left_inverse right_inverse : category morphism. Hint Rewrite @left_inverse @right_inverse : category. Hint Rewrite @left_inverse @right_inverse : morphism. @@ -216,7 +216,7 @@ Section iso_equiv_relation. end. End iso_equiv_relation. -#[global] +#[export] Hint Immediate isisomorphism_inverse : typeclass_instances. (** ** Epimorphisms and Monomorphisms *) @@ -377,9 +377,9 @@ Section EpiMono. End iso. End EpiMono. -#[global] Hint Immediate isisomorphism_inverse : typeclass_instances. +#[export] Hint Immediate isisomorphism_inverse : typeclass_instances. -#[global] +#[export] Hint Immediate isepimorphism_identity ismonomorphism_identity ismonomorphism_compose isepimorphism_compose @@ -464,7 +464,7 @@ Section iso_lemmas. Defined. End iso_lemmas. -#[global] +#[export] Hint Extern 1 (@IsIsomorphism _ _ _ (@morphism_of ?C ?D ?F ?s ?d ?m)) => apply (@iso_functor C D F s d m) : typeclass_instances. diff --git a/theories/Categories/Comma/Core.v b/theories/Categories/Comma/Core.v index 557a0a8ae2e..e6b0d6baebb 100644 --- a/theories/Categories/Comma/Core.v +++ b/theories/Categories/Comma/Core.v @@ -297,9 +297,9 @@ Qed. End category. *) -#[global] +#[export] Hint Unfold compose identity : category. -#[global] +#[export] Hint Constructors morphism object : category. (** ** (co)slice category [(a / F)], [(F / a)] *) diff --git a/theories/Categories/Functor/Composition/Laws.v b/theories/Categories/Functor/Composition/Laws.v index d06d5b89d2f..222066e268d 100644 --- a/theories/Categories/Functor/Composition/Laws.v +++ b/theories/Categories/Functor/Composition/Laws.v @@ -42,7 +42,7 @@ End identity_lemmas. Hint Rewrite @left_identity @right_identity : category. Hint Rewrite @left_identity @right_identity : functor. -#[global] +#[export] Hint Immediate left_identity right_identity : category functor. Section composition_lemmas. @@ -66,7 +66,7 @@ Section composition_lemmas. := @path_functor_uncurried_fst _ _ _ ((H o G) o F) (H o (G o F)) 1%path 1%path. End composition_lemmas. -#[global] +#[export] Hint Resolve associativity : category functor. Section coherence. diff --git a/theories/Categories/Functor/Core.v b/theories/Categories/Functor/Core.v index 947dc560cde..ef3ce2a9d0c 100644 --- a/theories/Categories/Functor/Core.v +++ b/theories/Categories/Functor/Core.v @@ -60,7 +60,7 @@ Module Export FunctorCoreNotations. Notation "F '_1' m" := (morphism_of F m) : morphism_scope. End FunctorCoreNotations. -#[global] +#[export] Hint Resolve composition_of identity_of : category functor. Hint Rewrite identity_of : category. Hint Rewrite identity_of : functor. diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v index ae39b259e96..6d881254cf3 100644 --- a/theories/Categories/FunctorCategory/Morphisms.v +++ b/theories/Categories/FunctorCategory/Morphisms.v @@ -37,10 +37,10 @@ Proof. - exact (apD10 (ap components_of right_inverse) x). Defined. -#[global] +#[export] Hint Immediate isisomorphism_components_of : typeclass_instances. (** When one of the functors is the identity functor, we fail to match correctly, because [apply] is stupid. So we do its work for it. *) -#[global] +#[export] Hint Extern 10 (@IsIsomorphism _ _ _ (@components_of ?C ?D ?F ?G ?T ?x)) => apply (fun H' => @isisomorphism_components_of _ C D F G T H' x) : typeclass_instances. @@ -73,7 +73,7 @@ Proof. ). Defined. -#[global] +#[export] Hint Immediate isisomorphism_natural_transformation : typeclass_instances. (** ** Variant of [idtoiso] for natural transformations *) diff --git a/theories/Categories/NatCategory.v b/theories/Categories/NatCategory.v index 73aa46610bf..134efd99b32 100644 --- a/theories/Categories/NatCategory.v +++ b/theories/Categories/NatCategory.v @@ -54,7 +54,7 @@ Module Export Core. End NatCategoryCoreNotations. Typeclasses Transparent nat_category. - #[global] + #[export] Hint Unfold nat_category : core. Arguments nat_category / . End Core. diff --git a/theories/Categories/NaturalTransformation/Core.v b/theories/Categories/NaturalTransformation/Core.v index a677d181735..038dbe09721 100644 --- a/theories/Categories/NaturalTransformation/Core.v +++ b/theories/Categories/NaturalTransformation/Core.v @@ -64,7 +64,7 @@ Global Arguments components_of {C D}%category {F G}%functor T%natural_transforma Global Arguments commutes {C D F G} !T / _ _ _ : rename. Global Arguments commutes_sym {C D F G} !T / _ _ _ : rename. -#[global] +#[export] Hint Resolve commutes : category natural_transformation. (** ** Helper lemmas *) diff --git a/theories/Categories/PseudonaturalTransformation/Core.v b/theories/Categories/PseudonaturalTransformation/Core.v index 5432e65c1f2..89e65127091 100644 --- a/theories/Categories/PseudonaturalTransformation/Core.v +++ b/theories/Categories/PseudonaturalTransformation/Core.v @@ -229,5 +229,5 @@ Create HintDb pseuodnatural_transformation discriminated. Arguments p_components_of {_} {X}%category {F G}%pseudofunctor T%pseudonatural_transformation a%object : rename, simpl nomatch. -#[global] +#[export] Hint Resolve p_commutes_respects_identity p_commutes_respects_composition : category pseudonatural_transformation. diff --git a/theories/Categories/Structure/Core.v b/theories/Categories/Structure/Core.v index 8ef73800fb9..33414e82711 100644 --- a/theories/Categories/Structure/Core.v +++ b/theories/Categories/Structure/Core.v @@ -106,7 +106,7 @@ Global Existing Instance istrunc_is_structure_homomorphism. Create HintDb structure_homomorphisms discriminated. -#[global] +#[export] Hint Resolve is_structure_homomorphism_identity is_structure_homomorphism_composition : structure_homomorphisms. (** When [(P, H)] is a notion of structure, for [α β : P x] we define diff --git a/theories/Classes/implementations/pointwise.v b/theories/Classes/implementations/pointwise.v index 51e8879fb01..628fd97f45c 100644 --- a/theories/Classes/implementations/pointwise.v +++ b/theories/Classes/implementations/pointwise.v @@ -72,7 +72,7 @@ Section contents. Defined. End contents. -#[global] +#[export] Hint Resolve associativity absorption diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v index 1280767b1dc..456fbdd483f 100644 --- a/theories/Classes/interfaces/abstract_algebra.v +++ b/theories/Classes/interfaces/abstract_algebra.v @@ -48,7 +48,7 @@ Section setoid_morphisms. End setoid_morphisms. (* HOTT TODO check if this is ok/useful *) -#[global] +#[export] Hint Extern 4 (?f _ = ?f _) => eapply (ap f) : core. Section setoid_binary_morphisms. @@ -156,13 +156,13 @@ Section upper_classes. End upper_classes. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 4 (PropHolds (1 <> 0)) => eapply @intdom_nontrivial : typeclass_instances. -#[global] +#[export] Hint Extern 5 (PropHolds (1 ≶ 0)) => eapply @field_nontrivial : typeclass_instances. -#[global] +#[export] Hint Extern 5 (PropHolds (1 <> 0)) => eapply @decfield_nontrivial : typeclass_instances. @@ -172,7 +172,7 @@ Integers -> IntegralDomain -> Ring and sometimes directly. Making this an instance with a low priority instead of using intdom_ring:> IsRing forces Coq to take the right way *) -#[global] +#[export] Hint Extern 10 (IsRing _) => apply @intdom_ring : typeclass_instances. Arguments recip_inverse {A Aplus Amult Azero Aone Anegate Aap Arecip IsField} _. @@ -286,7 +286,7 @@ End jections. Global Instance isinj_idmap A : @IsInjective A A idmap := fun x y => idmap. -#[global] +#[export] Hint Unfold IsInjective : typeclass_instances. Section strong_injective. diff --git a/theories/Classes/interfaces/canonical_names.v b/theories/Classes/interfaces/canonical_names.v index f79ff83f453..e3bdf332758 100644 --- a/theories/Classes/interfaces/canonical_names.v +++ b/theories/Classes/interfaces/canonical_names.v @@ -48,7 +48,7 @@ Class TrivialApart A {Aap : Apart A} := ; trivial_apart : forall x y, x ≶ y <-> x <> y }. Definition sig_apart `{Apart A} (P: A -> Type) : Apart (sig P) := fun x y => x.1 ≶ y.1. -#[global] +#[export] Hint Extern 10 (Apart (sig _)) => apply @sig_apart : typeclass_instances. Class Cast A B := cast: A -> B. @@ -92,11 +92,11 @@ Instance join_is_sg_op `{f : Join A} : SgOp A := f. Instance top_is_mon_unit `{s : Top A} : MonUnit A := s. Instance bottom_is_mon_unit `{s : Bottom A} : MonUnit A := s. -#[global] +#[export] Hint Extern 4 (Apart (ApartZero _)) => apply @sig_apart : typeclass_instances. -#[global] +#[export] Hint Extern 4 (Apart (NonNeg _)) => apply @sig_apart : typeclass_instances. -#[global] +#[export] Hint Extern 4 (Apart (Pos _)) => apply @sig_apart : typeclass_instances. (* Notations: *) @@ -186,11 +186,11 @@ Ltac auto_trans := match goal with [ H: ?R ?x ?y, I: ?R ?y ?z |- ?R ?x ?z] => apply (transitivity H I) end. -#[global] +#[export] Hint Extern 2 (?x ≤ ?y) => reflexivity : core. -#[global] +#[export] Hint Extern 4 (?x ≤ ?z) => auto_trans : core. -#[global] +#[export] Hint Extern 4 (?x < ?z) => auto_trans : core. Class Abs A `{Le A} `{Zero A} `{Negate A} @@ -419,7 +419,7 @@ Arguments enumerator_issurj A {_} _. *) Class PropHolds (P : Type) := prop_holds: P. -#[global] +#[export] Hint Extern 0 (PropHolds _) => assumption : typeclass_instances. Ltac solve_propholds := diff --git a/theories/Classes/interfaces/orders.v b/theories/Classes/interfaces/orders.v index 99a35c3f17b..1e36d3d14da 100644 --- a/theories/Classes/interfaces/orders.v +++ b/theories/Classes/interfaces/orders.v @@ -110,9 +110,9 @@ Section srorder_maps. ; strict_order_embedding_reflecting :> StrictlyOrderReflecting }. End srorder_maps. -#[global] +#[export] Hint Extern 4 (?f _ ≤ ?f _) => apply (order_preserving f) : core. -#[global] +#[export] Hint Extern 4 (?f _ < ?f _) => apply (strictly_order_preserving f) : core. (* @@ -154,10 +154,10 @@ Class FullPseudoSemiRingOrder `{Apart A} `{Plus A} ; full_pseudo_srorder_le_iff_not_lt_flip : forall x y, x ≤ y <-> ~(y < x) }. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 7 (PropHolds (0 < _ * _)) => eapply @pos_mult_compat : typeclass_instances. -#[global] +#[export] Hint Extern 7 (PropHolds (0 ≤ _ * _)) => eapply @nonneg_mult_compat : typeclass_instances. diff --git a/theories/Classes/orders/dec_fields.v b/theories/Classes/orders/dec_fields.v index fae205607df..d6b39dda91b 100644 --- a/theories/Classes/orders/dec_fields.v +++ b/theories/Classes/orders/dec_fields.v @@ -108,9 +108,9 @@ Qed. End contents. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 12 (PropHolds (0 ≤ _)) => eapply @nonneg_dec_recip_compat : typeclass_instances. -#[global] +#[export] Hint Extern 12 (PropHolds (0 < _)) => eapply @pos_dec_recip_compat : typeclass_instances. diff --git a/theories/Classes/orders/maps.v b/theories/Classes/orders/maps.v index 1a54ed6e640..d8ad21c852d 100644 --- a/theories/Classes/orders/maps.v +++ b/theories/Classes/orders/maps.v @@ -305,13 +305,13 @@ Section composition. OrderEmbedding f -> OrderEmbedding g -> OrderEmbedding (g ∘ f) := {}. End composition. -#[global] +#[export] Hint Extern 4 (OrderPreserving (_ ∘ _)) => class_apply @compose_order_preserving : typeclass_instances. -#[global] +#[export] Hint Extern 4 (OrderReflecting (_ ∘ _)) => class_apply @compose_order_reflecting : typeclass_instances. -#[global] +#[export] Hint Extern 4 (OrderEmbedding (_ ∘ _)) => class_apply @compose_order_embedding : typeclass_instances. diff --git a/theories/Classes/orders/naturals.v b/theories/Classes/orders/naturals.v index 01e6a77fd97..81278eeb4fa 100644 --- a/theories/Classes/orders/naturals.v +++ b/theories/Classes/orders/naturals.v @@ -92,5 +92,5 @@ Section another_ring. End another_ring. End naturals_order. -#[global] +#[export] Hint Extern 20 (PropHolds (_ ≤ _)) => eapply @nat_nonneg : typeclass_instances. diff --git a/theories/Classes/orders/orders.v b/theories/Classes/orders/orders.v index 32278bd20cd..603483c0d2a 100644 --- a/theories/Classes/orders/orders.v +++ b/theories/Classes/orders/orders.v @@ -314,13 +314,13 @@ Section full_partial_order. End full_partial_order. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 5 (PropHolds (_ <> _)) => eapply @strict_po_apart_ne : typeclass_instances. -#[global] +#[export] Hint Extern 10 (PropHolds (_ ≤ _)) => eapply @lt_le : typeclass_instances. -#[global] +#[export] Hint Extern 20 (Decidable (_ < _)) => eapply @lt_dec_slow : typeclass_instances. @@ -415,14 +415,14 @@ Section full_pseudo_order. Defined. End full_pseudo_order. -#[global] +#[export] Hint Extern 8 (Decidable (_ < _)) => eapply @lt_dec : typeclass_instances. (* The following instances would be tempting, but turn out to be a bad idea. -#[global] +#[export] Hint Extern 10 (PropHolds (_ <> _)) => eapply @le_ne : typeclass_instances. -#[global] +#[export] Hint Extern 10 (PropHolds (_ <> _)) => eapply @le_ne_flip : typeclass_instances. It will then loop like: diff --git a/theories/Classes/orders/semirings.v b/theories/Classes/orders/semirings.v index 5383b2dc7b9..678bc94da9b 100644 --- a/theories/Classes/orders/semirings.v +++ b/theories/Classes/orders/semirings.v @@ -182,7 +182,7 @@ Section semiring_order. End semiring_order. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 7 (PropHolds (0 ≤ _ + _)) => eapply @nonneg_plus_compat : typeclass_instances. @@ -346,7 +346,7 @@ Section strict_semiring_order. End strict_semiring_order. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 7 (PropHolds (0 < _ + _)) => eapply @pos_plus_compat : typeclass_instances. @@ -559,15 +559,15 @@ Section pseudo_semiring_order. Qed. End pseudo_semiring_order. -#[global] +#[export] Hint Extern 7 (PropHolds (0 < 1)) => eapply @lt_0_1 : typeclass_instances. -#[global] +#[export] Hint Extern 7 (PropHolds (0 < 2)) => eapply @lt_0_2 : typeclass_instances. -#[global] +#[export] Hint Extern 7 (PropHolds (0 < 3)) => eapply @lt_0_3 : typeclass_instances. -#[global] +#[export] Hint Extern 7 (PropHolds (0 < 4)) => eapply @lt_0_4 : typeclass_instances. -#[global] +#[export] Hint Extern 7 (PropHolds (2 ≶ 0)) => eapply @apart_0_2 : typeclass_instances. Section full_pseudo_semiring_order. @@ -800,13 +800,13 @@ Section full_pseudo_semiring_order. End full_pseudo_semiring_order. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 7 (PropHolds (0 ≤ 1)) => eapply @le_0_1 : typeclass_instances. -#[global] +#[export] Hint Extern 7 (PropHolds (0 ≤ 2)) => eapply @le_0_2 : typeclass_instances. -#[global] +#[export] Hint Extern 7 (PropHolds (0 ≤ 3)) => eapply @le_0_3 : typeclass_instances. -#[global] +#[export] Hint Extern 7 (PropHolds (0 ≤ 4)) => eapply @le_0_4 : typeclass_instances. Section dec_semiring_order. @@ -950,17 +950,17 @@ Section another_semiring_strict. End another_semiring_strict. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 15 (PropHolds (_ ≤ _ _)) => eapply @preserves_nonneg : typeclass_instances. -#[global] +#[export] Hint Extern 15 (PropHolds (_ < _ _)) => eapply @preserves_pos : typeclass_instances. (* Oddly enough, the above hints do not work for goals of the following shape? *) -#[global] +#[export] Hint Extern 15 (PropHolds (_ ≤ '_)) => eapply @preserves_nonneg : typeclass_instances. -#[global] +#[export] Hint Extern 15 (PropHolds (_ < '_)) => eapply @preserves_pos : typeclass_instances. diff --git a/theories/Classes/theory/apartness.v b/theories/Classes/theory/apartness.v index 31c6a09be30..56c4a11d329 100644 --- a/theories/Classes/theory/apartness.v +++ b/theories/Classes/theory/apartness.v @@ -23,7 +23,7 @@ Qed. End contents. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 3 (PropHolds (_ <> _)) => eapply @apart_ne : typeclass_instances. Lemma projected_strong_setoid `{IsApart B} `{Apart A} `{IsHSet A} diff --git a/theories/Classes/theory/dec_fields.v b/theories/Classes/theory/dec_fields.v index 2575d94f64a..46a92231167 100644 --- a/theories/Classes/theory/dec_fields.v +++ b/theories/Classes/theory/dec_fields.v @@ -177,7 +177,7 @@ Qed. End contents. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 7 (PropHolds (/ _ <> 0)) => eapply @dec_recip_ne_0 : typeclass_instances. diff --git a/theories/Classes/theory/fields.v b/theories/Classes/theory/fields.v index 33fe87bc4ec..c86cd0b51a3 100644 --- a/theories/Classes/theory/fields.v +++ b/theories/Classes/theory/fields.v @@ -272,10 +272,10 @@ Qed. End field_properties. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 8 (PropHolds (// _ ≶ 0)) => eapply @recip_apart_zero : typeclass_instances. -#[global] +#[export] Hint Extern 8 (PropHolds (_ * _ ≶ 0)) => eapply @mult_apart_zero : typeclass_instances. diff --git a/theories/Classes/theory/groups.v b/theories/Classes/theory/groups.v index 000bdd541b4..dde7e145a73 100644 --- a/theories/Classes/theory/groups.v +++ b/theories/Classes/theory/groups.v @@ -293,23 +293,23 @@ Section compose_mor. End compose_mor. -#[global] +#[export] Hint Extern 4 (IsSemiGroupPreserving (_ ∘ _)) => class_apply @compose_sg_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsMonoidPreserving (_ ∘ _)) => class_apply @compose_monoid_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsSemiGroupPreserving (_ o _)) => class_apply @compose_sg_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsMonoidPreserving (_ o _)) => class_apply @compose_monoid_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsSemiGroupPreserving (_^-1)) => class_apply @invert_sg_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsMonoidPreserving (_^-1)) => class_apply @invert_monoid_morphism : typeclass_instances. diff --git a/theories/Classes/theory/lattices.v b/theories/Classes/theory/lattices.v index 13ac5d8e36d..fbe8280e653 100644 --- a/theories/Classes/theory/lattices.v +++ b/theories/Classes/theory/lattices.v @@ -229,27 +229,27 @@ Section morphism_composition. Qed. End morphism_composition. -#[global] +#[export] Hint Extern 4 (IsJoinPreserving (_ ∘ _)) => class_apply @compose_join_sl_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsMeetPreserving (_ ∘ _)) => class_apply @compose_meet_sl_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsBoundedJoinPreserving (_ ∘ _)) => class_apply @compose_bounded_join_sl_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsLatticePreserving (_ ∘ _)) => class_apply @compose_lattice_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsJoinPreserving (_^-1)) => class_apply @invert_join_sl_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsMeetPreserving (_^-1)) => class_apply @invert_meet_sl_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsBoundedJoinPreserving (_^-1)) => class_apply @invert_bounded_join_sl_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsLatticePreserving (_^-1)) => class_apply @invert_lattice_morphism : typeclass_instances. diff --git a/theories/Classes/theory/naturals.v b/theories/Classes/theory/naturals.v index 4147082bbd4..4061490f540 100644 --- a/theories/Classes/theory/naturals.v +++ b/theories/Classes/theory/naturals.v @@ -242,9 +242,9 @@ End with_a_ring. End contents. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 6 (PropHolds (1 <> 0)) => eapply @nat_nontrivial : typeclass_instances. -#[global] +#[export] Hint Extern 6 (PropHolds (1 ≶ 0)) => eapply @nat_nontrivial_apart : typeclass_instances. diff --git a/theories/Classes/theory/rings.v b/theories/Classes/theory/rings.v index 40033e166dc..96e7d6c74a7 100644 --- a/theories/Classes/theory/rings.v +++ b/theories/Classes/theory/rings.v @@ -128,7 +128,7 @@ Section semiring_props. End semiring_props. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 3 (PropHolds (_ * _ <> 0)) => eapply @mult_ne_0 : typeclass_instances. Section semiringmor_props. @@ -180,7 +180,7 @@ Section semiringmor_props. End semiringmor_props. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 12 (PropHolds (_ _ <> 0)) => eapply @isinjective_ne_0 : typeclass_instances. @@ -368,7 +368,7 @@ Section integral_domain_props. End integral_domain_props. (* Due to bug #2528 *) -#[global] +#[export] Hint Extern 6 (PropHolds (1 ≶ 0)) => eapply @intdom_nontrivial_apart : typeclass_instances. @@ -469,9 +469,9 @@ Section morphism_composition. Qed. End morphism_composition. -#[global] +#[export] Hint Extern 4 (IsSemiRingPreserving (_ ∘ _)) => class_apply @compose_sr_morphism : typeclass_instances. -#[global] +#[export] Hint Extern 4 (IsSemiRingPreserving (_^-1)) => class_apply @invert_sr_morphism : typeclass_instances. diff --git a/theories/Modalities/Modality.v b/theories/Modalities/Modality.v index 64815d30265..d57f77dcea4 100644 --- a/theories/Modalities/Modality.v +++ b/theories/Modalities/Modality.v @@ -146,7 +146,7 @@ Defined. Coercion modality_to_reflective_subuniverse : Modality >-> ReflectiveSubuniverse. (** Unfortunately, sometimes [modality_subuniv] pops up anyway. The following hint helps typeclass inference look through it. *) -#[global] +#[export] Hint Extern 0 (In (modality_subuniv _) _) => progress change modality_subuniv with (rsu_subuniv o modality_to_reflective_subuniverse) in * : typeclass_instances. (** Modalities are precisely the reflective subuniverses that are [<<] themselves. *) diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v index fd0fef64ebf..9ad05fdcc1e 100644 --- a/theories/Modalities/ReflectiveSubuniverse.v +++ b/theories/Modalities/ReflectiveSubuniverse.v @@ -2062,6 +2062,6 @@ Proof. intros; rapply ooextendable_conn_map_inO. Defined. -#[global] Hint Immediate inO_isequiv_to_O : typeclass_instances. -#[global] Hint Immediate inO_unsigma : typeclass_instances. -#[global] Hint Immediate isconnected_conn_map_to_unit : typeclass_instances. +#[export] Hint Immediate inO_isequiv_to_O : typeclass_instances. +#[export] Hint Immediate inO_unsigma : typeclass_instances. +#[export] Hint Immediate isconnected_conn_map_to_unit : typeclass_instances. diff --git a/theories/Spaces/Finite.v b/theories/Spaces/Finite.v index 87c2afd0b49..e09eedaa54b 100644 --- a/theories/Spaces/Finite.v +++ b/theories/Spaces/Finite.v @@ -468,7 +468,7 @@ Proof. - refine (finite_equiv Empty nx^-1 _). Defined. -#[global] +#[export] Hint Immediate finite_decidable_hprop : typeclass_instances. (** It follows that the propositional truncation of any finite set is finite. *) diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v index b9d56ec4c87..20c23a83f06 100644 --- a/theories/Truncations/Connectedness.v +++ b/theories/Truncations/Connectedness.v @@ -80,7 +80,7 @@ Defined. End Extensions. -#[global] Hint Immediate conn_point_incl : typeclass_instances. +#[export] Hint Immediate conn_point_incl : typeclass_instances. (** ** Decreasing connectedness *) diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v index f333dffd724..3ed1d8f52ed 100644 --- a/theories/Truncations/Core.v +++ b/theories/Truncations/Core.v @@ -137,7 +137,7 @@ Defined. (** Instead, we make the latter an immediate instance, but with high cost (i.e. low priority) so that it doesn't override the ordinary lemmas about truncation. Unfortunately, [Hint Immediate] doesn't allow specifying a cost, so we use [Hint Extern] instead. *) (** Hint Immediate istrunc_inO_tr : typeclass_instances. *) (** See https://github.com/coq/coq/issues/11697 *) -#[global] +#[export] Hint Extern 1000 (IsTrunc _ _) => simple apply istrunc_inO_tr; solve [ trivial ] : typeclass_instances. (** This doesn't seem to be quite the same as [Hint Immediate] with a different cost either, though; see the comment in the proof of [Trunc_min] below. *) @@ -158,7 +158,7 @@ Proof. assumption. Defined. -#[global] +#[export] Hint Immediate istruncmap_mapinO_tr : typeclass_instances. (** ** A few special things about the (-1)-truncation. *) diff --git a/theories/Types/Equiv.v b/theories/Types/Equiv.v index b3949383f13..aff96470c76 100644 --- a/theories/Types/Equiv.v +++ b/theories/Types/Equiv.v @@ -189,5 +189,5 @@ Section AssumeFunext. End AssumeFunext. (** We make this a global hint outside of the section. *) -#[global] +#[export] Hint Immediate isequiv_contr_map : typeclass_instances. diff --git a/theories/Types/Sigma.v b/theories/Types/Sigma.v index 5c3f58b4cf2..c64281e71d1 100644 --- a/theories/Types/Sigma.v +++ b/theories/Types/Sigma.v @@ -629,7 +629,7 @@ Global Instance isequiv_path_sigma_hprop {A P} `{forall x : A, IsHProp (P x)} {u : IsEquiv (@path_sigma_hprop A P _ u v) | 100 := isequiv_compose. -#[global] +#[export] Hint Immediate isequiv_path_sigma_hprop : typeclass_instances. Definition equiv_path_sigma_hprop {A : Type} {P : A -> Type} @@ -643,7 +643,7 @@ Definition isequiv_pr1_path_hprop {A} {P : A -> Type} : IsEquiv (@pr1_path A P x y) := _ : IsEquiv (path_sigma_hprop x y)^-1. -#[global] +#[export] Hint Immediate isequiv_pr1_path_hprop : typeclass_instances. (** We define this for ease of [SearchAbout IsEquiv ap pr1] *) diff --git a/theories/WildCat/Type.v b/theories/WildCat/Type.v index 4106c8a7deb..5d0cf786b9e 100644 --- a/theories/WildCat/Type.v +++ b/theories/WildCat/Type.v @@ -78,7 +78,7 @@ Proof. assumption. Defined. -#[global] +#[export] Hint Immediate catie_isequiv : typeclass_instances. Global Instance isinitial_zero : IsInitial Empty. From b8359c1a64976200da7570b155829f7c46671152 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 19 Jan 2021 18:04:50 +0100 Subject: [PATCH 7/9] removed unused variables --- theories/Classes/implementations/family_prod.v | 4 ++-- theories/Spaces/Finite.v | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Classes/implementations/family_prod.v b/theories/Classes/implementations/family_prod.v index d01d038572b..ec59b6ec0d7 100644 --- a/theories/Classes/implementations/family_prod.v +++ b/theories/Classes/implementations/family_prod.v @@ -43,7 +43,7 @@ Section family_prod. (P : ∀ i, F i -> Type) : FamilyProd F ℓ → Type := match ℓ with | nil => λ _, True - | i :: ℓ' => λ '(x,s), P i x ∧ for_all_family_prod F P s + | i :: _ => λ '(x,s), P i x ∧ for_all_family_prod F P s end. (** [for_all_2_family_prod F G R (x1,...,xn,tt) (y1,...,yn,tt) = True] @@ -54,7 +54,7 @@ Section family_prod. : FamilyProd F ℓ → FamilyProd G ℓ → Type := match ℓ with | nil => λ _ _, True - | i :: ℓ' => λ '(x,s) '(y,t), R i x y ∧ for_all_2_family_prod F G R s t + | i :: _ => λ '(x,s) '(y,t), R i x y ∧ for_all_2_family_prod F G R s t end. (** If [R : ∀ i, relation (F i)] is a family of relations indexed by diff --git a/theories/Spaces/Finite.v b/theories/Spaces/Finite.v index e09eedaa54b..d49ec920036 100644 --- a/theories/Spaces/Finite.v +++ b/theories/Spaces/Finite.v @@ -66,7 +66,7 @@ Defined. Fixpoint fin_zero {n : nat} : Fin n.+1 := match n with | O => inr tt - | S n' => inl fin_zero + | S _ => inl fin_zero end. (** Where `fin_zero` computes the first element of Fin (S n), `fin_last` computes the last. *) From cd36f2fb16d258b8f11f945be6d6fcaae09b89ba Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 19 Jan 2021 18:06:10 +0100 Subject: [PATCH 8/9] changed Numeral notation to Number --- theories/Spaces/Int/Core.v | 2 +- theories/Spaces/Pos/Core.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Spaces/Int/Core.v b/theories/Spaces/Int/Core.v index 772498d067e..6e3e6945347 100644 --- a/theories/Spaces/Int/Core.v +++ b/theories/Spaces/Int/Core.v @@ -85,7 +85,7 @@ Definition int_of_decimal_int (d : Decimal.int) : Int := end end. -Numeral Notation Int int_of_decimal_int int_to_decimal_int : int_scope. +Number Notation Int int_of_decimal_int int_to_decimal_int : int_scope. (* For some reason 0 can be parsed as an integer, but is printed as [zero]. This notation fixes that. *) Notation "0" := zero : int_scope. diff --git a/theories/Spaces/Pos/Core.v b/theories/Spaces/Pos/Core.v index 87650572b02..d966fd2ecd3 100644 --- a/theories/Spaces/Pos/Core.v +++ b/theories/Spaces/Pos/Core.v @@ -404,5 +404,5 @@ Definition pos_to_uint p := Decimal.rev (pos_to_little_uint p). Definition pos_to_decimal_int n := Decimal.Pos (pos_to_uint n). -Numeral Notation Pos pos_of_decimal_int pos_to_uint : positive_scope. +Number Notation Pos pos_of_decimal_int pos_to_uint : positive_scope. From ab002bbfec036a250293bcac76d1a248720dff57 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 19 Jan 2021 18:07:23 +0100 Subject: [PATCH 9/9] replaced Grab Existential Variables with Unshelve --- theories/Categories/Adjoint/HomCoercions.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Categories/Adjoint/HomCoercions.v b/theories/Categories/Adjoint/HomCoercions.v index c1692599f63..a673b4ed220 100644 --- a/theories/Categories/Adjoint/HomCoercions.v +++ b/theories/Categories/Adjoint/HomCoercions.v @@ -212,7 +212,7 @@ Section AdjunctionEquivalences'. _ _ _ _ (equiv_isequiv (equiv_hom_set_adjunction T (fst cd) (snd cd))^-1)). - Grab Existential Variables. + Unshelve. simpl. intros. exact (adjunction_hom__of__adjunction_unit__commutes T _ _ _ _ _ _).