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

neg => Qneg :-)
---

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