dependence to legacy/coq.ma fixed

diff --git a/helm/software/matita/tests/absurd.ma b/helm/software/matita/tests/absurd.ma
index fe789a00f9eab4c44181b0900e15abd14acead6d..3a9719e413f0624f44fe7e3307ce676427e28cc2 100644 (file)
--- a/helm/software/matita/tests/absurd.ma
+++ b/helm/software/matita/tests/absurd.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/absurd/".
-include "legacy/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/software/matita/tests/apply.ma b/helm/software/matita/tests/apply.ma
index abd4a940700657dc505a46616a5514ffb6286db5..a77c99ca1324dab64649c3d379f2b5186ed85133 100644 (file)
--- a/helm/software/matita/tests/apply.ma
+++ b/helm/software/matita/tests/apply.ma
@@ -14,7 +14,7 @@
 
 (* test _with_ the WHD on the apply argument *)
 set "baseuri" "cic:/matita/tests/apply/".
-include "legacy/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)".

diff --git a/helm/software/matita/tests/assumption.ma b/helm/software/matita/tests/assumption.ma
index ef84002ac5a8621c721d3d1f5077370a444c0e60..fca9ca907bbceb1b555926b1000e6c75524bebc8 100644 (file)
--- a/helm/software/matita/tests/assumption.ma
+++ b/helm/software/matita/tests/assumption.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/assumption".
-include "legacy/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/software/matita/tests/bad_tests/auto.ma b/helm/software/matita/tests/bad_tests/auto.ma
index 24226600c6669657629fb9afdd9a274034d72bcb..2972bfa62344f14744c98ef5bd2534b4577c51a6 100755 (executable)
--- a/helm/software/matita/tests/bad_tests/auto.ma
+++ b/helm/software/matita/tests/bad_tests/auto.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/auto/".
-include "legacy/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/software/matita/tests/bool.ma b/helm/software/matita/tests/bool.ma
index 2b7f815b98afb95e5fb19c90ffe2e6b85a1b52a5..e94d7c285ed5960c8a35d7d289c800e6e2082a56 100644 (file)
--- a/helm/software/matita/tests/bool.ma
+++ b/helm/software/matita/tests/bool.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/tests/bool/".
 
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".

diff --git a/helm/software/matita/tests/change.ma b/helm/software/matita/tests/change.ma
index b2ae3b7a05cbfaf44784daa4c027a71316fa208b..e415dd8181cc104ea7072110fe1c1b9c1aaf5145 100644 (file)
--- a/helm/software/matita/tests/change.ma
+++ b/helm/software/matita/tests/change.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/change/".
-include "legacy/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/software/matita/tests/clear.ma b/helm/software/matita/tests/clear.ma
index 5aaf6c0d60f204055e10f275201108af4166fcc6..617965258d92dd7f464435181c493422bfd230a2 100644 (file)
--- a/helm/software/matita/tests/clear.ma
+++ b/helm/software/matita/tests/clear.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/clear".
-include "legacy/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/software/matita/tests/clearbody.ma b/helm/software/matita/tests/clearbody.ma
index ca4b9316e87008495379637778f8ad5375dfd018..5b6b4ada736b481abbbe0a0de3ae793478358e1c 100644 (file)
--- a/helm/software/matita/tests/clearbody.ma
+++ b/helm/software/matita/tests/clearbody.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/clearbody".
-include "legacy/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/software/matita/tests/comments.ma b/helm/software/matita/tests/comments.ma
index 41e8e9bb35663375a49143f75cf57e421578cadd..cb54a90d3aeb7db62afd76140478a4f5aa1d11e5 100644 (file)
--- a/helm/software/matita/tests/comments.ma
+++ b/helm/software/matita/tests/comments.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/comments/".
-include "legacy/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/software/matita/tests/constructor.ma b/helm/software/matita/tests/constructor.ma
index 7ea26d43c540debb5de6b5b3e1af75ed3f1d5d7b..f33044f12ba740937aede424c89a9b4b19a1cbd6 100644 (file)
--- a/helm/software/matita/tests/constructor.ma
+++ b/helm/software/matita/tests/constructor.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/constructor".
-include "legacy/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/software/matita/tests/continuationals.ma b/helm/software/matita/tests/continuationals.ma
index bb531961a3a28c172d7f7275450a0000c60eddc3..a9d85ce2544d98b10c544c0de10cc5a052cc612b 100644 (file)
--- a/helm/software/matita/tests/continuationals.ma
+++ b/helm/software/matita/tests/continuationals.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/continuationals".
-include "legacy/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/software/matita/tests/contradiction.ma b/helm/software/matita/tests/contradiction.ma
index 305a862cfd464b14a830e456f928559c5a68c7a9..ed1ef6b3c035e1f5173093223b57225a34939585 100644 (file)
--- a/helm/software/matita/tests/contradiction.ma
+++ b/helm/software/matita/tests/contradiction.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/contradiction".
-include "legacy/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/software/matita/tests/cut.ma b/helm/software/matita/tests/cut.ma
index a30fe2fabb38b0c38b0f5757d54510b1d039e193..24d17f13d1d1193d711f0a18bf98e761c4262374 100644 (file)
--- a/helm/software/matita/tests/cut.ma
+++ b/helm/software/matita/tests/cut.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/cut".
-include "legacy/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/software/matita/tests/decompose.ma b/helm/software/matita/tests/decompose.ma
index fe72f710a7a4b8fed5dfba289fee2ae411768a26..03f43a9ca505a24d93b63d9840a9251e7c12f294 100644 (file)
--- a/helm/software/matita/tests/decompose.ma
+++ b/helm/software/matita/tests/decompose.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/decompose".
-include "legacy/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/software/matita/tests/demodulation_coq.ma b/helm/software/matita/tests/demodulation_coq.ma
index 57fccac5da2bddc1f1f5e95bfec41a98e840d303..c2a77e96ab10bdd29da945a7b9bd22844b03d024 100644 (file)
--- a/helm/software/matita/tests/demodulation_coq.ma
+++ b/helm/software/matita/tests/demodulation_coq.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/demodulation/".
 
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 alias num = "natural number".
 alias symbol "times" = "Coq's natural times".

diff --git a/helm/software/matita/tests/dependent_injection.ma b/helm/software/matita/tests/dependent_injection.ma
index 28991acf43cfcf55cc07ef6ef3cb5047126d4927..069c7529744115802f655e2cd69b3f7a3ddb113a 100644 (file)
--- a/helm/software/matita/tests/dependent_injection.ma
+++ b/helm/software/matita/tests/dependent_injection.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/tests/dependent_injection".
 
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".

diff --git a/helm/software/matita/tests/discriminate.ma b/helm/software/matita/tests/discriminate.ma
index 8b655de87bf8135c3494b88bea6ddcd2d5dbb682..81c2da87fbf381b9d8954088a41ee9ce44c465cb 100644 (file)
--- a/helm/software/matita/tests/discriminate.ma
+++ b/helm/software/matita/tests/discriminate.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/discriminate".
-include "legacy/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".
@@ -68,4 +68,4 @@ qed.
 theorem recursive: S (S (S O)) = S (S O) \to False.
  intros;
  destruct H.
-qed.
\ No newline at end of file
+qed.

diff --git a/helm/software/matita/tests/elim.ma b/helm/software/matita/tests/elim.ma
index d6a4c3f33f7e994f362100e40ec391b0702ce569..03eafba6a0075dbedf19b75289873dde2e793e57 100644 (file)
--- a/helm/software/matita/tests/elim.ma
+++ b/helm/software/matita/tests/elim.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/elim".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 inductive stupidtype: Set \def
   | Base : stupidtype

diff --git a/helm/software/matita/tests/fguidi.ma b/helm/software/matita/tests/fguidi.ma
index fab765baff7f2b4de9621ff67aa509190a793fdf..84faee59ace814a772bacd076c95c6c6ef7ec662 100644 (file)
--- a/helm/software/matita/tests/fguidi.ma
+++ b/helm/software/matita/tests/fguidi.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/fguidi/".
-include "legacy/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/software/matita/tests/fix_betareduction.ma b/helm/software/matita/tests/fix_betareduction.ma
index 508a4056b22d32c343025d0ddf91e6ad6dbcc4c3..65c916f17183adcf9067832e93ba456ae788218e 100644 (file)
--- a/helm/software/matita/tests/fix_betareduction.ma
+++ b/helm/software/matita/tests/fix_betareduction.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/fix_betareduction/".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
 alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con".

diff --git a/helm/software/matita/tests/fold.ma b/helm/software/matita/tests/fold.ma
index a8cee102119bcbf9c46f86eefe27a8fab075cb7c..cd507c7de845a90a990977f3a42bf897fd64b431 100644 (file)
--- a/helm/software/matita/tests/fold.ma
+++ b/helm/software/matita/tests/fold.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/fold".
-include "legacy/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/software/matita/tests/generalize.ma b/helm/software/matita/tests/generalize.ma
index 68492baa3a206c5aa14256dec4fadd20b8b539ce..58634434a394491e95ebaf648da84d658389d318 100644 (file)
--- a/helm/software/matita/tests/generalize.ma
+++ b/helm/software/matita/tests/generalize.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/generalize".
-include "legacy/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/software/matita/tests/hard_refine.ma b/helm/software/matita/tests/hard_refine.ma
index 1b194559c28b97918b8d184c57027f1aab23c9e9..94766ab0b06ba67c81c31ac3d65c1a1dfb8aeb81 100644 (file)
--- a/helm/software/matita/tests/hard_refine.ma
+++ b/helm/software/matita/tests/hard_refine.ma
@@ -1,5 +1,5 @@
 set "baseuri" "cic:/matita/TPTP/BOO024-1".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
 (* Inclusion of: BOO024-1.p *)
 (* -------------------------------------------------------------------------- *)

diff --git a/helm/software/matita/tests/injection.ma b/helm/software/matita/tests/injection.ma
index 69edcf6205ea8ccaee3fd29d76f05bc7f4b92b06..929e63cd5296fadb329a6b806a731667ac377741 100644 (file)
--- a/helm/software/matita/tests/injection.ma
+++ b/helm/software/matita/tests/injection.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/tests/injection".
 
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".

diff --git a/helm/software/matita/tests/inversion.ma b/helm/software/matita/tests/inversion.ma
index 925c54677ed4d0f61fd2b242caa9c9e09025e39e..07d3a0c4a09f9e90ef82a7048559b473f4517fd7 100644 (file)
--- a/helm/software/matita/tests/inversion.ma
+++ b/helm/software/matita/tests/inversion.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/inversion_sum/".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 
 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".

diff --git a/helm/software/matita/tests/inversion2.ma b/helm/software/matita/tests/inversion2.ma
index 5fc9c93350c857d1c553cc844a9debcb200cff67..c99c59bcf7f77321d8c00aaef0f799e5d4d786d7 100644 (file)
--- a/helm/software/matita/tests/inversion2.ma
+++ b/helm/software/matita/tests/inversion2.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/inversion2/".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 inductive nat : Set \def
    O : nat

diff --git a/helm/software/matita/tests/metasenv_ordering.ma b/helm/software/matita/tests/metasenv_ordering.ma
index fc354e6aed5e2f5d2d3ea1d4111bb88c6475891e..de9746d527130f3c3a9c5715c6977118a67c8c9e 100644 (file)
--- a/helm/software/matita/tests/metasenv_ordering.ma
+++ b/helm/software/matita/tests/metasenv_ordering.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/tests/metasenv_ordering".
 
-include "legacy/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/software/matita/tests/paramodulation.ma b/helm/software/matita/tests/paramodulation.ma
index 311b9455a6fe4d3b1535fdced868108094cbdb51..d23384d9e5b9c6478795b3a5d38dfb56f2650358 100644 (file)
--- a/helm/software/matita/tests/paramodulation.ma
+++ b/helm/software/matita/tests/paramodulation.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/paramodulation".
-include "legacy/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/software/matita/tests/paramodulation/boolean_algebra.ma b/helm/software/matita/tests/paramodulation/boolean_algebra.ma
index 0450a752c64e5f80f3b53b1d6a274eb03a05a86f..0d3e16f5d12b3bf6153f434a9a0029c823bc9d05 100644 (file)
--- a/helm/software/matita/tests/paramodulation/boolean_algebra.ma
+++ b/helm/software/matita/tests/paramodulation/boolean_algebra.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/SK/".
 
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".

diff --git a/helm/software/matita/tests/paramodulation/group.ma b/helm/software/matita/tests/paramodulation/group.ma
index 97e2afe179d58ceb9e1d31af594d73bc5dcfd22b..a19884d05451c25f7adf9963453ac2482830c6d8 100644 (file)
--- a/helm/software/matita/tests/paramodulation/group.ma
+++ b/helm/software/matita/tests/paramodulation/group.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/tests/paramodulation/group".
 
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".

diff --git a/helm/software/matita/tests/replace.ma b/helm/software/matita/tests/replace.ma
index b740f387ef032e5f6c795ecdac86bcffe10d7f9e..843075766405b8bcea9a77443ce68e00cfdc6759 100644 (file)
--- a/helm/software/matita/tests/replace.ma
+++ b/helm/software/matita/tests/replace.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/replace/".
-include "legacy/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/software/matita/tests/rewrite.ma b/helm/software/matita/tests/rewrite.ma
index 580ad13ed524bba3bbf99b98a578879e8b270491..c262613f226756ee0166f1ce2ba9d8dbd6958d9c 100644 (file)
--- a/helm/software/matita/tests/rewrite.ma
+++ b/helm/software/matita/tests/rewrite.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/rewrite/".
-include "legacy/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/software/matita/tests/simpl.ma b/helm/software/matita/tests/simpl.ma
index 89812286985c0080428f038b205a8375ed28cd1b..61150e817b42df9406d078bbdd48afb2a91591b0 100644 (file)
--- a/helm/software/matita/tests/simpl.ma
+++ b/helm/software/matita/tests/simpl.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/simpl/".
-include "legacy/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/software/matita/tests/test2.ma b/helm/software/matita/tests/test2.ma
index 92d9a533068de44e1e009051ac6acb0543609506..93da2eccee94aa4b7237fb509e1f398d84fa6809 100644 (file)
--- a/helm/software/matita/tests/test2.ma
+++ b/helm/software/matita/tests/test2.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/test2/".
-include "legacy/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/software/matita/tests/test3.ma b/helm/software/matita/tests/test3.ma
index 08d4cbcb6a0f49783da0959e0af7b1779063391e..5753f37af6923167e1ba9f5f5d44daccc5973019 100644 (file)
--- a/helm/software/matita/tests/test3.ma
+++ b/helm/software/matita/tests/test3.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/test3/".
-include "legacy/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/software/matita/tests/test4.ma b/helm/software/matita/tests/test4.ma
index 6c3b7ec6f356040b3781cbeba55c0a59ac8dee9f..55cfb6aaf15be6171ffb0296e162ccb442d31edf 100644 (file)
--- a/helm/software/matita/tests/test4.ma
+++ b/helm/software/matita/tests/test4.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/test4/".
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 
 (* commento che va nell'ast, ma non viene contato

diff --git a/helm/software/matita/tests/unfold.ma b/helm/software/matita/tests/unfold.ma
index 99f3931c21780ea24fdf625228027df9727c570e..3318db17db5db75d782723017357a972465f2c4f 100644 (file)
--- a/helm/software/matita/tests/unfold.ma
+++ b/helm/software/matita/tests/unfold.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/unfold".
 
-include "legacy/coq.ma".
+include "../legacy/coq.ma".
 
 alias symbol "plus" (instance 0) = "Coq's natural plus".
 definition myplus \def \lambda x,y. x+y.