X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FBasics.ma;h=5d9ba4c2e2be7c99b2c7bc9838b2c023569c4653;hb=52206fa1c090fcdc8386ec8d7e88beca089c7e39;hp=22f1f819a59b0df0de278501f96ed4580ec9b287;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/algebra/Basics.ma b/matita/contribs/CoRN-Decl/algebra/Basics.ma
index 22f1f819a..5d9ba4c2e 100644
--- a/matita/contribs/CoRN-Decl/algebra/Basics.ma
+++ b/matita/contribs/CoRN-Decl/algebra/Basics.ma
@@ -75,6 +75,18 @@ Transparent sym_eq.
 Transparent f_equal.
 *)
 
+(* NOTATION
+Notation Pair := (pair (B:=_)).
+*)
+
+(* NOTATION
+Notation Proj1 := (proj1 (B:=_)).
+*)
+
+(* NOTATION
+Notation Proj2 := (proj2 (B:=_)).
+*)
+
 (* Following only needed in finite, but tha's now obsolete
 
 Lemma deMorgan_or_and: (A,B,X:Prop)((A\/B)->X)->(A->X)/\(B->X).
@@ -132,7 +144,7 @@ coercion. *)
 
 (* begin hide *)
 
-coercion "cic:/matita/CoRN-Decl/algebra/Basics/Z_of_nat.con" 0 (* compounds *).
+coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *).
 
 (* end hide *)