- transcript: bugfix

[helm.git] / helm / software / matita / library / Q / q / qtimes.ma

diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma
index 3b4b24b7971179f25ca96747d2bef57cc6a7bfad..f03b8687cff5c174ed818cf0471bae3dd864ae44 100644 (file)
--- 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;