X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Flibrary%2Fnat%2Fplus.ma;h=1c145dd6141cea519fd99f7c681a179159a72346;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=6067ebcdcd6b87ffde1fe7bce0059627e6723fb7;hpb=3eff4cc36820df9faddb3cb16390717851db499c;p=helm.git

diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 6067ebcdc..1c145dd61 100644
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -21,8 +21,8 @@ let rec plus n m \def
  [ O \Rightarrow m
  | (S p) \Rightarrow S (plus p m) ].
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural plus" 'plus x y = (cic:/matita/nat/plus/plus.con x y).
-alias symbol "plus" (instance 0) = "natural plus".
 
 theorem plus_n_O: \forall n:nat. n = n+O.
 intros.elim n.