Update to latest HoTT library

_CoqProject

@@ -50,6 +50,7 @@ theories/Init.v
 theories/Signature.v
 theories/CoreTactics.v
 
+theories/Prop/SigmaNotations.v
 theories/Prop/Logic.v
 theories/Prop/Classes.v
 theories/Prop/EqDec.v

test-suite/BasicsHoTT.v

@@ -9,7 +9,7 @@ From Equations Require Import CoreTactics.
 Require Import Equations.HoTT.All Equations.HoTT.WellFounded.
 Require Import Coq.Unicode.Utf8.
 Require HoTT.Basics.Overture.
-Require Import HoTT.Types.Bool HoTT.Spaces.Nat.
+Require Import HoTT.Types.Bool HoTT.Spaces.Nat HoTT.Spaces.List.Core.
 
 Local Open Scope nat_scope.
 
@@ -180,7 +180,7 @@ equal (S n) (S m) with equal n m => {
   equal (S n) (S m) (inr p) := inr (λ{ | idpath => p idpath }) } ;
 equal x y := inr _.
 
-Notation "[]" := (@Datatypes.nil _) (at level 0) : list_scope.
+Notation "[]" := (@List.Core.nil _) (at level 0) : list_scope.
 Local Open Scope list_scope.
 
 Equations app_with {A} (l l' : list A) : list A :=
@@ -236,7 +236,7 @@ Tactic Notation "myreplace" constr(c) "with" constr(d) "by" tactic(tac) :=
 Lemma rev_rev_acc : forall {A} (l : list A), rev_acc l [] = rev l.
 Proof.
   intros. myreplace (rev l) with (rev l +++ []) by (symmetry; apply app'_nil).
-  generalize (@Datatypes.nil A).
+  generalize (@List.Core.nil A).
   funelim (rev l).
   - intros. reflexivity.
   - intros l'. autorewrite with rev_acc. rewrite X.

theories/CoreTactics.v

@@ -11,7 +11,6 @@
 Require Export Equations.Init.
 Require Import Equations.Signature.
 
-Import Sigma_Notations.
 Local Open Scope equations_scope.
 
 (** Try to find a contradiction. *)

theories/HoTT/DepElim.v

@@ -653,7 +653,7 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "
 
 (** [solve_equation] is used to prove the equation lemmas for an existing definition.  *)
 
-Ltac exfalso := cut False; [intros []|].
+Ltac exfalso := cut Empty; [intros []|].
 
 Ltac find_empty := simpl in * ; exfalso ;
   match goal with

theories/HoTT/EqDecInstances.v

@@ -10,12 +10,12 @@ From Equations Require Import Init.
 Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.DepElim
         Equations.HoTT.Constants
         Equations.HoTT.Tactics Equations.HoTT.EqDec Equations.HoTT.NoConfusion.
+From HoTT Require Import Spaces.List.Core.
 Local Open Scope equations_scope.
 Import Sigma_Notations.
 
 Set Universe Polymorphism.
 
-
 (** Tactic to solve EqDec goals, destructing recursive calls for the recursive
   structure of the type and calling instances of eq_dec on other types. *)
 

theories/HoTT/FunctionalInduction.v

@@ -9,7 +9,7 @@
 Set Warnings "-notation-overridden".
 Require Import Equations.CoreTactics.
 Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.DepElim.
-Require Import HoTT.Basics.Datatypes HoTT.Spaces.Nat.
+Require Import HoTT.Spaces.Nat.
 
 Local Open Scope nat_scope.
 Local Open Scope equations_scope.

theories/HoTT/Logic.v

@@ -1,5 +1,7 @@
 From Equations Require Import Init.
 Require Export HoTT.Basics.Overture.
+Require Export HoTT.Basics.Tactics.
+
 Set Warnings "-notation-overridden".
 Set Universe Polymorphism.
 
@@ -35,3 +37,21 @@ Definition transport_r {A} (P : A -> Type) {x y : A} (e : y = x) : P x -> P y :=
 Lemma paths_rect_dep_r {A} (x : A) (P : forall a, a = x -> Type) (p : P x 1%path)
       (y : A) (e : y = x) : P y e.
 Proof. destruct e. apply p. Defined.
+
+Module Sigma_Notations.
+
+Notation "'Σ' x .. y , P" := (sigma (fun x => .. (sigma (fun y => P)) ..))
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' Σ  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Notation "( x , .. , y , z )" :=
+  (@sigmaI _ _ x .. (@sigmaI _ _ y z) ..)
+      (right associativity, at level 0,
+       format "( x ,  .. ,  y ,  z )") : equations_scope.
+
+Notation "x .1" := (Equations.Init.pr1 x) : equations_scope.
+Notation "x .2" := (Equations.Init.pr2 x) : equations_scope.
+
+End Sigma_Notations.
+
+Import Sigma_Notations.

theories/HoTT/NoConfusion.v

@@ -16,12 +16,14 @@ From Equations Require Import Init Signature.
 Require Import Equations.CoreTactics.
 Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Constants.
 Require Import Equations.HoTT.DepElim Equations.HoTT.Tactics.
+Require Import HoTT.Spaces.List.Core.
+
 
 (** Parameterized inductive types just need NoConfusion. *)
 
 Local Set Universe Minimization ToSet.
 
-Derive NoConfusion for Unit Bool.Bool nat option sum Datatypes.prod list.
+Derive NoConfusion for Unit Bool.Bool nat option sum prod list.
 
 #[export] Instance Bool_depelim : DependentEliminationPackage Bool.Bool :=
   { elim := @Bool.Bool_ind }.

theories/HoTT/Relation.v

@@ -14,6 +14,7 @@ Set Warnings "-notation-overridden".
 Require Import Equations.HoTT.Logic.
 
 Local Open Scope equations_scope.
+
 Import Sigma_Notations.
 
 (** Relations in Type *)
@@ -191,6 +192,8 @@ Section Swap.
     | sp_swap x y (p:A * A) : symprod A A R R (pair x y) p -> swapprod (pair y x) p.
 End Swap.
 
+Local Open Scope equations_scope.
+From HoTT Require Import Spaces.List.Core.
 Local Open Scope list_scope.
 
 Section Lexicographic_Exponentiation.

theories/HoTT/Relation_Properties.v

@@ -337,8 +337,8 @@ Section Properties.
     Lemma clos_rst_rst1n  : forall x y,
       clos_refl_sym_trans R x y -> clos_refl_sym_trans_1n R x y.
       induction 1.
-      - constructor 2 with y; auto with Relations.
-        constructor 1.
+      - constructor 2 with y; auto with Relations;
+        constructor 1; assumption.
       - constructor 1.
       - apply clos_rst1n_sym; auto.
       - eapply clos_rst1n_trans; eauto.

theories/HoTT/Telescopes.v

@@ -43,7 +43,7 @@ Section TeleSigma.
   Equations tele_rel : tele -> tele -> Type :=
   | tip A | tip B := A -> B -> Type;
   | ext A B | ext A' B' := forall (x : A) (y : A'), tele_rel (B x) (B' y);
-  | _ | _ := False.
+  | _ | _ := Empty.
 
   Equations tele_rel_app (T U : tele) (P : tele_rel T U) (x : tele_sigma T) (y : tele_sigma U) : Type :=
   tele_rel_app (tip A) (tip A') P a a' := P a a';

theories/Init.v

@@ -76,27 +76,6 @@ Arguments sigmaI {A} B pr1 pr2.
 
 Extraction Inline pr1 pr2.
 
-Set Warnings "-notation-overridden".
-
-Module Sigma_Notations.
-
-Notation "'Σ' x .. y , P" := (sigma (fun x => .. (sigma (fun y => P)) ..))
-  (at level 200, x binder, y binder, right associativity,
-  format "'[  ' '[  ' Σ  x  ..  y ']' ,  '/' P ']'") : type_scope.
-
-Notation "( x , .. , y , z )" :=
-  (@sigmaI _ _ x .. (@sigmaI _ _ y z) ..)
-      (right associativity, at level 0,
-       format "( x ,  .. ,  y ,  z )") : equations_scope.
-
-Notation " x .1 " := (pr1 x) : equations_scope.
-Notation " x .2 " := (pr2 x) : equations_scope.
-
-End Sigma_Notations.
-
-Import Sigma_Notations.
-
-
 (** Forward reference for the no-confusion tactic. *)
 Ltac noconf H := fail "Equations.Init.noconf has not been bound yet".
 

theories/Prop/Loader.v

@@ -15,6 +15,7 @@ Declare ML Module "coq-equations.plugin".
 
 From Equations Require Export Init Signature.
 Require Import Equations.CoreTactics.
+Require Export Equations.Prop.SigmaNotations.
 Require Export Equations.Prop.Classes.
 Require Import Equations.Prop.DepElim Equations.Prop.Constants.
 Require Export Equations.Prop.EqDec.

theories/Prop/Logic.v

@@ -1,4 +1,6 @@
 From Equations Require Import Init.
+From Equations.Prop Require Export SigmaNotations.
+
 From Coq Require Import Extraction Relation_Definitions.
 
 (** The regular dependent eliminator of equality *)

theories/Prop/SigmaNotations.v

@@ -0,0 +1,21 @@
+From Equations Require Import Init.
+
+Set Warnings "-notation-overridden".
+
+Module Sigma_Notations.
+
+Notation "'Σ' x .. y , P" := (sigma (fun x => .. (sigma (fun y => P)) ..))
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' Σ  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Notation "( x , .. , y , z )" :=
+  (@sigmaI _ _ x .. (@sigmaI _ _ y z) ..)
+      (right associativity, at level 0,
+       format "( x ,  .. ,  y ,  z )") : equations_scope.
+
+Notation "x .1" := (pr1 x) : equations_scope.
+Notation "x .2" := (pr2 x) : equations_scope.
+
+End Sigma_Notations.
+
+Import Sigma_Notations.

theories/Type/Logic.v

@@ -39,6 +39,24 @@ End Id_Notations.
 
 Import Id_Notations.
 
+Module Sigma_Notations.
+
+Notation "'Σ' x .. y , P" := (sigma (fun x => .. (sigma (fun y => P)) ..))
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' Σ  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Notation "( x , .. , y , z )" :=
+  (@sigmaI _ _ x .. (@sigmaI _ _ y z) ..)
+      (right associativity, at level 0,
+       format "( x ,  .. ,  y ,  z )") : equations_scope.
+
+Notation "x .1" := (pr1 x) : equations_scope.
+Notation "x .2" := (pr2 x) : equations_scope.
+
+End Sigma_Notations.
+
+Import Sigma_Notations.
+
 Section IdTheory.
   Universe i.
   Context {A : Type@{i}}.