switch to Int in cring_Z

test/Algebra/Rings/Matrix.v

@@ -1,7 +1,7 @@
 From HoTT Require Import Basics.
 From HoTT Require Import Algebra.Rings.Matrix.
 From HoTT Require Import Spaces.Nat.Core Spaces.List.Core.
-From HoTT Require Import Algebra.Rings.Z Spaces.BinInt.Core Algebra.Rings.CRing.
+From HoTT Require Import Algebra.Rings.Z Spaces.Int Algebra.Rings.CRing.
 From HoTT Require Import Classes.interfaces.canonical_names.
 
 Local Open Scope mc_scope.
@@ -38,7 +38,7 @@ Definition test2_B := Build_Matrix' nat 4 4
 
 Definition test2 : entries test2_A = entries test2_B := idpath.
 
-Local Open Scope binint_scope.
+Local Open Scope int_scope.
 
 (** Matrices with ring entries can be multiplied *)
 

theories/Algebra/AbGroups/Cyclic.v

@@ -1,6 +1,6 @@
 Require Import Basics Types WildCat.Core Truncations.Core
   AbelianGroup AbHom Centralizer AbProjective
-  Groups.FreeGroup AbGroups.Z BinInt.Core Spaces.Int.
+  Groups.FreeGroup AbGroups.Z Spaces.Int.
 
 (** * Cyclic groups *)
 
@@ -71,7 +71,7 @@ Defined.
 
 (** The map sending the generator to [1 : Int]. *)
 Definition Z1_to_Z `{Funext} : ab_Z1 $-> abgroup_Z
-  := Z1_rec (G:=abgroup_Z) 1%binint.
+  := Z1_rec (G:=abgroup_Z) 1%int.
 
 (** TODO:  Prove that [Z1_to_Z] is a group isomorphism. *)
 

theories/Algebra/AbGroups/Z.v

@@ -1,5 +1,5 @@
 Require Import Basics.
-Require Import Spaces.Pos.Core Spaces.BinInt.
+Require Import Spaces.Pos.Core Spaces.Int.
 Require Import Algebra.AbGroups.AbelianGroup.
 
 Local Set Universe Minimization ToSet.
@@ -8,17 +8,17 @@ Local Set Universe Minimization ToSet.
 
 (** See also Cyclic.v for a definition of the integers as the free group on one generator. *)
 
-Local Open Scope binint_scope.
+Local Open Scope int_scope.
 
 (** TODO: switch to [Int] *)
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.
-  - refine (Build_Group BinInt binint_add 0 binint_negation _); repeat split.
+  - refine (Build_Group Int int_add 0 int_neg _); repeat split.
     + exact _.
-    + exact binint_add_assoc.
-    + exact binint_add_0_r.
-    + exact binint_add_negation_l.
-    + exact binint_add_negation_r.
-  - exact binint_add_comm.
+    + exact int_add_assoc.
+    + exact int_add_0_r.
+    + exact int_add_neg_l.
+    + exact int_add_neg_r.
+  - exact int_add_comm.
 Defined.