From 9d9c3c7cbed6ea98b10421381d88c4d5a1fbf0f0 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 9 Jan 2006 13:56:10 +0000 Subject: [PATCH] changes location of coq.ma (now "legacy/coq.ma") --- helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma | 2 +- helm/matita/tests/absurd.ma | 2 +- helm/matita/tests/apply.ma | 4 ++-- helm/matita/tests/assumption.ma | 2 +- helm/matita/tests/bad_tests/auto.ma | 2 +- helm/matita/tests/change.ma | 2 +- helm/matita/tests/clear.ma | 2 +- helm/matita/tests/clearbody.ma | 2 +- helm/matita/tests/coercions.ma | 2 +- helm/matita/tests/comments.ma | 2 +- helm/matita/tests/constructor.ma | 2 +- helm/matita/tests/continuationals.ma | 2 +- helm/matita/tests/contradiction.ma | 2 +- helm/matita/tests/cut.ma | 2 +- helm/matita/tests/decompose.ma | 2 +- helm/matita/tests/discriminate.ma | 2 +- helm/matita/tests/elim.ma | 2 +- helm/matita/tests/fguidi.ma | 2 +- helm/matita/tests/fold.ma | 2 +- helm/matita/tests/generalize.ma | 2 +- helm/matita/tests/inversion.ma | 2 +- helm/matita/tests/inversion2.ma | 2 +- helm/matita/tests/metasenv_ordering.ma | 2 +- helm/matita/tests/paramodulation.ma | 2 +- helm/matita/tests/replace.ma | 2 +- helm/matita/tests/rewrite.ma | 2 +- helm/matita/tests/simpl.ma | 2 +- helm/matita/tests/test2.ma | 2 +- helm/matita/tests/test3.ma | 2 +- helm/matita/tests/test4.ma | 2 +- helm/matita/tests/unfold.ma | 2 +- 31 files changed, 32 insertions(+), 32 deletions(-) diff --git a/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma index 9a2c5fb9d..cf7848abe 100644 --- a/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma +++ b/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/terms_defs". -include "coq.ma". +include "legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". diff --git a/helm/matita/tests/absurd.ma b/helm/matita/tests/absurd.ma index 19c738d05..fe789a00f 100644 --- a/helm/matita/tests/absurd.ma +++ b/helm/matita/tests/absurd.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/absurd/". -include "coq.ma". +include "legacy/coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "not" = "cic:/Coq/Init/Logic/not.con". diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma index 21c0faa41..abd4a9407 100644 --- a/helm/matita/tests/apply.ma +++ b/helm/matita/tests/apply.ma @@ -14,7 +14,7 @@ (* test _with_ the WHD on the apply argument *) set "baseuri" "cic:/matita/tests/apply/". -include "coq.ma". +include "legacy/coq.ma". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". @@ -54,4 +54,4 @@ qed. term (to reveal a product) *) theorem d: \forall A: Prop. \lnot A \to A \to False. intros. apply H. assumption. -qed. \ No newline at end of file +qed. diff --git a/helm/matita/tests/assumption.ma b/helm/matita/tests/assumption.ma index fde8f8c98..ef84002ac 100644 --- a/helm/matita/tests/assumption.ma +++ b/helm/matita/tests/assumption.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/assumption". -include "coq.ma". +include "legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". diff --git a/helm/matita/tests/bad_tests/auto.ma b/helm/matita/tests/bad_tests/auto.ma index 5c6c04358..c7bd62492 100755 --- a/helm/matita/tests/bad_tests/auto.ma +++ b/helm/matita/tests/bad_tests/auto.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/auto/". -include "coq.ma". +include "legacy/coq.ma". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". diff --git a/helm/matita/tests/change.ma b/helm/matita/tests/change.ma index 16b675316..b2ae3b7a0 100644 --- a/helm/matita/tests/change.ma +++ b/helm/matita/tests/change.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/change/". -include "coq.ma". +include "legacy/coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/helm/matita/tests/clear.ma b/helm/matita/tests/clear.ma index 9f1655b59..5aaf6c0d6 100644 --- a/helm/matita/tests/clear.ma +++ b/helm/matita/tests/clear.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/clear". -include "coq.ma". +include "legacy/coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". diff --git a/helm/matita/tests/clearbody.ma b/helm/matita/tests/clearbody.ma index 0956cbc1e..ca4b9316e 100644 --- a/helm/matita/tests/clearbody.ma +++ b/helm/matita/tests/clearbody.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/clearbody". -include "coq.ma". +include "legacy/coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index 5429b1f82..20b15cd26 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/coercions/". -include "coq.ma". +include "legacy/coq.ma". inductive pos: Set \def | one : pos diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma index f9412f45a..41e8e9bb3 100644 --- a/helm/matita/tests/comments.ma +++ b/helm/matita/tests/comments.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/comments/". -include "coq.ma". +include "legacy/coq.ma". (* commento che va nell'ast, ma non viene contato come step perche' non e' un executable diff --git a/helm/matita/tests/constructor.ma b/helm/matita/tests/constructor.ma index 3ee7f4b98..7ea26d43c 100644 --- a/helm/matita/tests/constructor.ma +++ b/helm/matita/tests/constructor.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/constructor". -include "coq.ma". +include "legacy/coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/continuationals.ma b/helm/matita/tests/continuationals.ma index b2f906084..f45061bad 100644 --- a/helm/matita/tests/continuationals.ma +++ b/helm/matita/tests/continuationals.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/test/continuationals/". -include "coq.ma". +include "legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". diff --git a/helm/matita/tests/contradiction.ma b/helm/matita/tests/contradiction.ma index 886bc8c80..305a862cf 100644 --- a/helm/matita/tests/contradiction.ma +++ b/helm/matita/tests/contradiction.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/contradiction". -include "coq.ma". +include "legacy/coq.ma". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias num (instance 0) = "natural number". diff --git a/helm/matita/tests/cut.ma b/helm/matita/tests/cut.ma index 3e5605a10..a30fe2fab 100644 --- a/helm/matita/tests/cut.ma +++ b/helm/matita/tests/cut.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/cut". -include "coq.ma". +include "legacy/coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/decompose.ma b/helm/matita/tests/decompose.ma index caf2d5289..fe72f710a 100644 --- a/helm/matita/tests/decompose.ma +++ b/helm/matita/tests/decompose.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/decompose". -include "coq.ma". +include "legacy/coq.ma". alias symbol "and" (instance 0) = "Coq's logical and". alias symbol "or" (instance 0) = "Coq's logical or". diff --git a/helm/matita/tests/discriminate.ma b/helm/matita/tests/discriminate.ma index f873dd8f7..d8e4bf2e2 100644 --- a/helm/matita/tests/discriminate.ma +++ b/helm/matita/tests/discriminate.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/discriminate". -include "coq.ma". +include "legacy/coq.ma". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/elim.ma b/helm/matita/tests/elim.ma index 9d48bc970..67d7fada1 100644 --- a/helm/matita/tests/elim.ma +++ b/helm/matita/tests/elim.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/elim". -include "coq.ma". +include "legacy/coq.ma". inductive stupidtype: Set \def | Base : stupidtype diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index 567f15c97..c6eb2a9d8 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/fguidi/". -include "coq.ma". +include "legacy/coq.ma". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". diff --git a/helm/matita/tests/fold.ma b/helm/matita/tests/fold.ma index 003d45f47..a8cee1021 100644 --- a/helm/matita/tests/fold.ma +++ b/helm/matita/tests/fold.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/fold". -include "coq.ma". +include "legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/generalize.ma b/helm/matita/tests/generalize.ma index aca28ffdc..68492baa3 100644 --- a/helm/matita/tests/generalize.ma +++ b/helm/matita/tests/generalize.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/generalize". -include "coq.ma". +include "legacy/coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma index b39d839b0..3e49e0668 100644 --- a/helm/matita/tests/inversion.ma +++ b/helm/matita/tests/inversion.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/inversion_sum/". -include "coq.ma". +include "legacy/coq.ma". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/inversion2.ma b/helm/matita/tests/inversion2.ma index bb8d18980..1125212dc 100644 --- a/helm/matita/tests/inversion2.ma +++ b/helm/matita/tests/inversion2.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/inversion/". -include "coq.ma". +include "legacy/coq.ma". inductive nat : Set \def O : nat diff --git a/helm/matita/tests/metasenv_ordering.ma b/helm/matita/tests/metasenv_ordering.ma index 25c66594b..fc354e6ae 100644 --- a/helm/matita/tests/metasenv_ordering.ma +++ b/helm/matita/tests/metasenv_ordering.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/tests/metasenv_ordering". -include "coq.ma". +include "legacy/coq.ma". alias num (instance 0) = "natural number". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". diff --git a/helm/matita/tests/paramodulation.ma b/helm/matita/tests/paramodulation.ma index d918fb451..311b9455a 100644 --- a/helm/matita/tests/paramodulation.ma +++ b/helm/matita/tests/paramodulation.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/paramodulation". -include "coq.ma". +include "legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/helm/matita/tests/replace.ma b/helm/matita/tests/replace.ma index b5d1eb355..2b174af64 100644 --- a/helm/matita/tests/replace.ma +++ b/helm/matita/tests/replace.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/replace/". -include "coq.ma". +include "legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index a69e33d77..580ad13ed 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/rewrite/". -include "coq.ma". +include "legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma index 1001d2351..65e9d48a4 100644 --- a/helm/matita/tests/simpl.ma +++ b/helm/matita/tests/simpl.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/simpl/". -include "coq.ma". +include "legacy/coq.ma". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "plus" = "cic:/Coq/Init/Peano/plus.con". diff --git a/helm/matita/tests/test2.ma b/helm/matita/tests/test2.ma index 0ffdb8268..92d9a5330 100644 --- a/helm/matita/tests/test2.ma +++ b/helm/matita/tests/test2.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/test2/". -include "coq.ma". +include "legacy/coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias symbol "and" (instance 0) = "Coq's logical and". diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma index 98dc65c95..cdf54906d 100644 --- a/helm/matita/tests/test3.ma +++ b/helm/matita/tests/test3.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/test3/". -include "coq.ma". +include "legacy/coq.ma". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a:\forall x.x=x. diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma index d680378eb..6c3b7ec6f 100644 --- a/helm/matita/tests/test4.ma +++ b/helm/matita/tests/test4.ma @@ -13,7 +13,7 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/test4/". -include "coq.ma". +include "legacy/coq.ma". (* commento che va nell'ast, ma non viene contato diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma index d17e5a2da..99f3931c2 100644 --- a/helm/matita/tests/unfold.ma +++ b/helm/matita/tests/unfold.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/unfold". -include "coq.ma". +include "legacy/coq.ma". alias symbol "plus" (instance 0) = "Coq's natural plus". definition myplus \def \lambda x,y. x+y. -- 2.39.2