updated dependencies

Author: Paolo Torrini

theories/cat.v

@@ -1199,6 +1199,11 @@ Notation pb s := (prepullback_isTerminal _ _ _ _ s).
 
 Notation "P <=> Q" := ((P -> Q) * (Q -> P))%type (at level 70).
 
+Notation "'sigma' x .. y , p" :=
+  (sigT (fun x => .. (sigT (fun y => p)) ..))
+  (at level 200, x binder, right associativity,
+   format "'[' 'sigma'  '/ ' x .. y ,  '/ ' p ']'")
+  : cat_scope.
 
 (**********************************************************************)
 

theories/encat.v

@@ -13,12 +13,13 @@ Local Open Scope algebra_scope.
 
 Local Open Scope cat_scope.
 
+(*
 Notation "'sigma' x .. y , p" :=
   (sigT (fun x => .. (sigT (fun y => p)) ..))
   (at level 200, x binder, right associativity,
    format "'[' 'sigma'  '/ ' x .. y ,  '/ ' p ']'")
   : type_scope.
-
+*)
 
 (*** DOUBLE CATEGORIES (REVISED) *)
 

theories/encatD.v

@@ -13,12 +13,13 @@ Local Open Scope algebra_scope.
 
 Local Open Scope cat_scope.
 
+(*
 Notation "'sigma' x .. y , p" :=
   (sigT (fun x => .. (sigT (fun y => p)) ..))
   (at level 200, x binder, right associativity,
    format "'[' 'sigma'  '/ ' x .. y ,  '/ ' p ']'")
   : type_scope.
-
+*)
 
 (********************************************************************)
 

theories/encatI.v

@@ -13,11 +13,13 @@ Local Open Scope algebra_scope.
 
 Local Open Scope cat_scope.
 
+(*
 Notation "'sigma' x .. y , p" :=
   (sigT (fun x => .. (sigT (fun y => p)) ..))
   (at level 200, x binder, right associativity,
    format "'[' 'sigma'  '/ ' x .. y ,  '/ ' p ']'")
   : type_scope.
+*)
 
 (*** GENERALISED ENRICHED CATEGORIES *)
 

theories/encatI0.v

@@ -13,12 +13,13 @@ Local Open Scope algebra_scope.
 
 Local Open Scope cat_scope.
 
+(*
 Notation "'sigma' x .. y , p" :=
   (sigT (fun x => .. (sigT (fun y => p)) ..))
   (at level 200, x binder, right associativity,
    format "'[' 'sigma'  '/ ' x .. y ,  '/ ' p ']'")
   : type_scope.
-
+*)
 
 (*** CATEGORIES WITH PULLBACKS *)