From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 25 Oct 2007 17:10:25 +0000 (+0000)
Subject: neg => Qneg :-)
X-Git-Tag: make_still_working~5945
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=feb0db45a9547e9b1bb0c75dd6ccba43d4f1e168;p=helm.git

neg => Qneg :-)
---

diff --git a/helm/software/matita/library/Q/q.ma b/helm/software/matita/library/Q/q.ma
index 23ef52551..072532d7b 100644
--- 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)