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