changes location of coq.ma (now "legacy/coq.ma")

diff --git a/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/terms_defs.ma
index 9a2c5fb9d2ebd1df4704a47dbbfcc5ab701c511b..cf7848abee3fad0a73501f47ad30504e96465b97 100644 (file)
--- 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 19c738d054b1bf67f036993ee1eba2ee747cce0a..fe789a00f9eab4c44181b0900e15abd14acead6d 100644 (file)
--- 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 21c0faa419100b2958493aaee9f697b714c22a9d..abd4a940700657dc505a46616a5514ffb6286db5 100644 (file)
--- 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 fde8f8c98dccb929d1ebe93eee246f74d583567e..ef84002ac5a8621c721d3d1f5077370a444c0e60 100644 (file)
--- 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 5c6c043587966de99df4cc69f667073a0a71fe2f..c7bd62492ba953cac304ac22150965af3901b5e2 100755 (executable)
--- 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 16b6753167000a94134e3a1b32c7b2c4014f04a2..b2ae3b7a05cbfaf44784daa4c027a71316fa208b 100644 (file)
--- 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 9f1655b597fc6da3dc6b763334075a4e7ae9eb12..5aaf6c0d60f204055e10f275201108af4166fcc6 100644 (file)
--- 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 0956cbc1e2f89cafb6d195c5e9fcabf269b21ac8..ca4b9316e87008495379637778f8ad5375dfd018 100644 (file)
--- 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 5429b1f82fb0aa427e8d0e55180664b0e2d5c77a..20b15cd2650d8a7f7840d68696da39423af2248c 100644 (file)
--- 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 f9412f45a9eb39feeae55cf3070605ef2c05d840..41e8e9bb35663375a49143f75cf57e421578cadd 100644 (file)
--- 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 3ee7f4b9843f688728e7496c221895ba1326304f..7ea26d43c540debb5de6b5b3e1af75ed3f1d5d7b 100644 (file)
--- 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 b2f90608422fe4e0e9103342eeed6cdbd2049edb..f45061bad76ef276a3e7a8ffbac64f90f1fe0e82 100644 (file)
--- 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 886bc8c80273031be132f1963c3ab89ef7d84659..305a862cfd464b14a830e456f928559c5a68c7a9 100644 (file)
--- 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 3e5605a10464ec32a86f56ed8a699b530e983092..a30fe2fabb38b0c38b0f5757d54510b1d039e193 100644 (file)
--- 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 caf2d52890bb5b239fe01432017bcce9f621a7bc..fe72f710a7a4b8fed5dfba289fee2ae411768a26 100644 (file)
--- 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 f873dd8f722e09d87d4ac5a3131bcbd0a356f196..d8e4bf2e25a84951c358c1437551c0d5a971d105 100644 (file)
--- 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 9d48bc970ecd46c576942a3911f45b7d974527fe..67d7fada10a01b0ac27c98625c1d6770127c4c99 100644 (file)
--- 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 567f15c97c88ca976c0ecf8b71b389df700da752..c6eb2a9d860585466af29e3811e6d409cd16bafb 100644 (file)
--- 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 003d45f4784440ea515a715e4f47ca3e72858a51..a8cee102119bcbf9c46f86eefe27a8fab075cb7c 100644 (file)
--- 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 aca28ffdcc2ddc9c2d9fdd335461507311a3c1d7..68492baa3a206c5aa14256dec4fadd20b8b539ce 100644 (file)
--- 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 b39d839b00cfe80a56bcd08bee4593cc846d73fc..3e49e06685d22818abd961fec9774f7708b4ab79 100644 (file)
--- 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 bb8d18980b7badef80226b24f50e1bbd276ec2aa..1125212dcd9c0bb86d58d8a47ac71cf099531951 100644 (file)
--- 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 25c66594bc0f644bc07dd4f1cc3bbe22fd0844d5..fc354e6aed5e2f5d2d3ea1d4111bb88c6475891e 100644 (file)
--- 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 d918fb4511ccf88566d6ea9f91852a12225144fe..311b9455a6fe4d3b1535fdced868108094cbdb51 100644 (file)
--- 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 b5d1eb355514bec21c75b0775e3bfffd01c82b8e..2b174af6478ff4917ac71137a11cc104af6c5d8b 100644 (file)
--- 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 a69e33d77c73915f30470fb3f11537df0695b1fc..580ad13ed524bba3bbf99b98a578879e8b270491 100644 (file)
--- 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 1001d2351f0b97a50da92ef8a48cad25b17b4c47..65e9d48a48c6e2f3467eacb56c3408c6a7a55459 100644 (file)
--- 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 0ffdb82682fb9f402965a304463f1074e037f786..92d9a533068de44e1e009051ac6acb0543609506 100644 (file)
--- 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 98dc65c9579c43ee0b22478e5a76e09662665708..cdf54906d1937e4cc0c309886bfdb480af80dfca 100644 (file)
--- 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 d680378ebc84efeeb7bfd09e9ee8d431b9b590ae..6c3b7ec6f356040b3781cbeba55c0a59ac8dee9f 100644 (file)
--- 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 d17e5a2daf9fd243c136f10cfcd6997707226ede..99f3931c21780ea24fdf625228027df9727c570e 100644 (file)
--- 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.