From 6e01bb1ae52fe45ce77a7f950efb5feb295e82b1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2007 17:10:25 +0000 Subject: [PATCH] neg => Qneg :-) --- matita/library/Q/q.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) -- 2.39.2