set "baseuri" "cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CPseudoMSpaces.v,v 1.3 2004/04/23 10:01:02 lcf Exp $ *)
inline "cic:/CoRN/metrics/CPseudoMSpaces/CPsMetricSpace.ind".
-coercion "cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces/cms_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/metrics/CPseudoMSpaces/cms_crr.con 0 (* compounds *).
(* UNEXPORTED
End Definition_PsMS0.
Implicit Arguments cms_d [c].
*)
+(* NOTATION
+Infix "[-d]" := cms_d (at level 68, left associativity).
+*)
+
(* UNEXPORTED
Section PsMS_axioms.
*)