neg => Qneg :-)

diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index 23ef525519b42282aa10185e14604e3a12fa8fcc..072532d7bc7a4c8732486f5886a9147f082d5523 100644 (file)
--- a/helm/software/matita/library/Q/q.ma
+++ b/helm/software/matita/library/Q/q.ma
@@ -330,7 +330,7 @@ definition Qtimes : Q \to Q \to Q \def
     |Qpos q1 \Rightarrow Qpos (rtimes p1 q1)
     |Qneg q1 \Rightarrow Qneg (rtimes p1 q1)
     ]
-  |neg p1 \Rightarrow 
+  |Qneg p1 \Rightarrow 
     match q with
     [OQ \Rightarrow OQ
     |Qpos q1 \Rightarrow Qneg (rtimes p1 q1)