More notation (up to where the open bugs allow me to put it without adding

[helm.git] / helm / matita / library / nat / times.ma

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index 24a756dc5c3b458b790eee6fa6d336ac991c54bd..d2ce51bfa83dd9605bf5160e227edf3c532aeff0 100644 (file)
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -23,6 +23,7 @@ let rec times n m \def
  [ O \Rightarrow O
  | (S p) \Rightarrow (m+(times p m)) ].
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
 
 theorem times_n_O: \forall n:nat. O = n*O.