X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq%2Fqtimes.ma;h=f03b8687cff5c174ed818cf0471bae3dd864ae44;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=3b4b24b7971179f25ca96747d2bef57cc6a7bfad;hpb=e85acd6f01bccc0b4a6750dd6d2710d7b511948a;p=helm.git

diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma
index 3b4b24b79..f03b8687c 100644
--- a/helm/software/matita/library/Q/q/qtimes.ma
+++ b/helm/software/matita/library/Q/q/qtimes.ma
@@ -33,7 +33,7 @@ definition Qtimes : Q \to Q \to Q \def
     ]
   ].
 
-interpretation "rational times" 'times x y = (cic:/matita/Q/q/qtimes/Qtimes.con x y).
+interpretation "rational times" 'times x y = (Qtimes x y).
 
 theorem Qtimes_q_OQ: ∀q. q * OQ = OQ.
  intro;