Merge pull request #1413 from Alizter/8.13

update to V8.13

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

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.
+#[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.
 
-Hint Resolve identity_refl: core.
+#[export] Hint Resolve identity_refl: core.
 
 Arguments identity {A} _ _.
 Arguments identity_refl {A a} , [A] a.

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.
+#[export] Hint Unfold not : core.
+#[export] Hint Resolve I : core.

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.
+#[export] Hint Immediate identity_sym not_identity_sym: core v62.

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.
+#[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.
-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.
-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).
-Hint Resolve f_equal2_plus : v62.
-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.
-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.
-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,21 +138,21 @@ 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.
+#[export] 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.
+#[export] Hint Resolve mult_n_O: core.
 
 Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
 Proof.
   intros; induction n as [| p H]; simpl; auto.
   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.
+#[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.
 
-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.
-Hint Unfold lt: core.
+#[export] Hint Unfold lt: core.
 
 Local Infix "<" := lt : nat_scope.
 
 Definition ge (n m:nat) := m <= n.
-Hint Unfold ge: core.
+#[export] Hint Unfold ge: core.
 
 Local Infix ">=" := ge : nat_scope.
 
 Definition gt (n m:nat) := m < n.
-Hint Unfold gt: core.
+#[export] Hint Unfold gt: core.
 
 Local Infix ">" := gt : nat_scope.
 

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.
+#[export] Hint Resolve existT existT2: core.

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.
+#[export] Hint Variables Opaque : rewrite.
 Create HintDb typeclass_instances discriminated.

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.

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]. *)
+#[export]
 Hint Extern 0 (IsEquiv _^-1) => apply @isequiv_inverse : typeclass_instances.
 
 (** [Equiv A B] is a symmetric relation. *)

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.
 
+#[export]
 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 /.
 
+#[export]
 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.
 
+#[export]
 Hint Extern 0 (IsTrunc_internal _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *)
 
+#[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. *)
+#[export]
 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).
 
+#[export]
 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? *)
+#[export]
 Hint Resolve idpath inverse : path_hints.
+#[export]
 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.
+#[export]
 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]. *)
+#[export]
 Hint Resolve tt : core.
 
 Register Unit as core.IDProp.type.

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).
 
+#[export]
 Hint Resolve
   concat_1p concat_p1 concat_p_pp
   inv_pp inv_V

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
@@ -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. *)
+#[export]
 Hint Immediate trunc_contr : typeclass_instances.
+#[export]
 Hint Immediate trunc_hprop : typeclass_instances.
+#[export]
 Hint Immediate trunc_hset : typeclass_instances.
 
 (** Equivalence preserves truncation (this is, of course, trivial with univalence).

theories/Categories/Adjoint/Composition/AssociativityLaw.v

@@ -47,4 +47,5 @@ Section composition_lemmas.
   Qed.
 End composition_lemmas.
 
+#[export]
 Hint Resolve associativity : category.

theories/Categories/Adjoint/Composition/IdentityLaws.v

@@ -52,4 +52,5 @@ Section identity_lemmas.
 End identity_lemmas.
 
 Hint Rewrite @left_identity @right_identity : category.
+#[export]
 Hint Immediate left_identity right_identity : category.

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 _ _ _ _ _ _).

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.
 
+#[export]
 Hint Resolve left_identity right_identity associativity : category morphism.
 Hint Rewrite left_identity right_identity : category.
 Hint Rewrite left_identity right_identity : morphism.

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.
 
+#[export]
 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.
 
+#[export]
 Hint Immediate isisomorphism_inverse : typeclass_instances.
 
 (** ** Epimorphisms and Monomorphisms *)
@@ -374,6 +377,9 @@ Section EpiMono.
   End iso.
 End EpiMono.
 
+#[export] Hint Immediate isisomorphism_inverse : typeclass_instances.
+
+#[export]
 Hint Immediate
   isepimorphism_identity ismonomorphism_identity
   ismonomorphism_compose isepimorphism_compose
@@ -458,6 +464,7 @@ Section iso_lemmas.
   Defined.
 End iso_lemmas.
 
+#[export]
 Hint Extern 1 (@IsIsomorphism _ _ _ (@morphism_of ?C ?D ?F ?s ?d ?m))
 => apply (@iso_functor C D F s d m) : typeclass_instances.
 

theories/Categories/Comma/Core.v

@@ -297,7 +297,9 @@ Qed.
   End category.
 *)
 
+#[export]
 Hint Unfold compose identity : category.
+#[export]
 Hint Constructors morphism object : category.
 
 (** ** (co)slice category [(a / F)], [(F / a)] *)

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.
+#[export]
 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.
 
+#[export]
 Hint Resolve associativity : category functor.
 
 Section coherence.

theories/Categories/Functor/Core.v

@@ -60,6 +60,7 @@ Module Export FunctorCoreNotations.
   Notation "F '_1' m" := (morphism_of F m) : morphism_scope.
 End FunctorCoreNotations.
 
+#[export]
 Hint Resolve composition_of identity_of : category functor.
 Hint Rewrite identity_of : category.
 Hint Rewrite identity_of : functor.