From de857819a83da112abf181019546f2684b921356 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 15 Oct 2007 11:22:24 +0000 Subject: [PATCH] Stupid bug fixed. --- helm/software/matita/tests/clearbody.ma | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/helm/software/matita/tests/clearbody.ma b/helm/software/matita/tests/clearbody.ma index 5b6b4ada7..3c95a8a1f 100644 --- a/helm/software/matita/tests/clearbody.ma +++ b/helm/software/matita/tests/clearbody.ma @@ -14,11 +14,10 @@ set "baseuri" "cic:/matita/tests/clearbody". include "../legacy/coq.ma". -alias num (instance 0) = "natural number". +alias num (instance 0) = "Coq natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". - theorem stupid : let x \def 0 + 1 in x + 2 = x + 2. intros. -- 2.39.2