From: Claudio Sacerdoti Coen Date: Mon, 15 Oct 2007 11:34:37 +0000 (+0000) Subject: natural number => Coq natural number X-Git-Tag: 0.4.95@7852~117 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f4f26fdfd2a627eef6bf27481e28833df05c82a;p=helm.git natural number => Coq natural number --- diff --git a/matita/tests/change.ma b/matita/tests/change.ma index e415dd818..214d0fbe3 100644 --- a/matita/tests/change.ma +++ b/matita/tests/change.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/tests/change/". 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". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". diff --git a/matita/tests/replace.ma b/matita/tests/replace.ma index ba1f41a8f..2961fdc7e 100644 --- a/matita/tests/replace.ma +++ b/matita/tests/replace.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/tests/replace/". include "../legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -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". alias symbol "times" (instance 0) = "Coq's natural times". diff --git a/matita/tests/rewrite.ma b/matita/tests/rewrite.ma index 1321be02c..dff3b2300 100644 --- a/matita/tests/rewrite.ma +++ b/matita/tests/rewrite.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/tests/rewrite/". include "../legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -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". alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".