From 0582a602f0b1d6f5430326893a473d78b0aa7dfd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 30 Dec 2006 18:59:14 +0000 Subject: [PATCH] dependence to legacy/coq.ma fixed --- helm/software/matita/tests/absurd.ma | 2 +- helm/software/matita/tests/apply.ma | 2 +- helm/software/matita/tests/assumption.ma | 2 +- helm/software/matita/tests/bad_tests/auto.ma | 2 +- helm/software/matita/tests/bool.ma | 2 +- helm/software/matita/tests/change.ma | 2 +- helm/software/matita/tests/clear.ma | 2 +- helm/software/matita/tests/clearbody.ma | 2 +- helm/software/matita/tests/comments.ma | 2 +- helm/software/matita/tests/constructor.ma | 2 +- helm/software/matita/tests/continuationals.ma | 2 +- helm/software/matita/tests/contradiction.ma | 2 +- helm/software/matita/tests/cut.ma | 2 +- helm/software/matita/tests/decompose.ma | 2 +- helm/software/matita/tests/demodulation_coq.ma | 2 +- helm/software/matita/tests/dependent_injection.ma | 2 +- helm/software/matita/tests/discriminate.ma | 4 ++-- helm/software/matita/tests/elim.ma | 2 +- helm/software/matita/tests/fguidi.ma | 2 +- helm/software/matita/tests/fix_betareduction.ma | 2 +- helm/software/matita/tests/fold.ma | 2 +- helm/software/matita/tests/generalize.ma | 2 +- helm/software/matita/tests/hard_refine.ma | 2 +- helm/software/matita/tests/injection.ma | 2 +- helm/software/matita/tests/inversion.ma | 2 +- helm/software/matita/tests/inversion2.ma | 2 +- helm/software/matita/tests/metasenv_ordering.ma | 2 +- helm/software/matita/tests/paramodulation.ma | 2 +- helm/software/matita/tests/paramodulation/boolean_algebra.ma | 2 +- helm/software/matita/tests/paramodulation/group.ma | 2 +- helm/software/matita/tests/replace.ma | 2 +- helm/software/matita/tests/rewrite.ma | 2 +- helm/software/matita/tests/simpl.ma | 2 +- helm/software/matita/tests/test2.ma | 2 +- helm/software/matita/tests/test3.ma | 2 +- helm/software/matita/tests/test4.ma | 2 +- helm/software/matita/tests/unfold.ma | 2 +- 37 files changed, 38 insertions(+), 38 deletions(-) diff --git a/helm/software/matita/tests/absurd.ma b/helm/software/matita/tests/absurd.ma index fe789a00f..3a9719e41 100644 --- 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 abd4a9407..a77c99ca1 100644 --- 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 ef84002ac..fca9ca907 100644 --- 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 24226600c..2972bfa62 100755 --- 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 2b7f815b9..e94d7c285 100644 --- 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 b2ae3b7a0..e415dd818 100644 --- 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 5aaf6c0d6..617965258 100644 --- 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 ca4b9316e..5b6b4ada7 100644 --- 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 41e8e9bb3..cb54a90d3 100644 --- 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 7ea26d43c..f33044f12 100644 --- 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 bb531961a..a9d85ce25 100644 --- 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 305a862cf..ed1ef6b3c 100644 --- 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 a30fe2fab..24d17f13d 100644 --- 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 fe72f710a..03f43a9ca 100644 --- 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 57fccac5d..c2a77e96a 100644 --- 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 28991acf4..069c75297 100644 --- 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 8b655de87..81c2da87f 100644 --- 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 d6a4c3f33..03eafba6a 100644 --- 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 fab765baf..84faee59a 100644 --- 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 508a4056b..65c916f17 100644 --- 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 a8cee1021..cd507c7de 100644 --- 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 68492baa3..58634434a 100644 --- 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 1b194559c..94766ab0b 100644 --- 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 69edcf620..929e63cd5 100644 --- 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 925c54677..07d3a0c4a 100644 --- 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 5fc9c9335..c99c59bcf 100644 --- 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 fc354e6ae..de9746d52 100644 --- 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 311b9455a..d23384d9e 100644 --- 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 0450a752c..0d3e16f5d 100644 --- 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 97e2afe17..a19884d05 100644 --- 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 b740f387e..843075766 100644 --- 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 580ad13ed..c262613f2 100644 --- 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 898122869..61150e817 100644 --- 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 92d9a5330..93da2ecce 100644 --- 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 08d4cbcb6..5753f37af 100644 --- 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 6c3b7ec6f..55cfb6aaf 100644 --- 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 99f3931c2..3318db17d 100644 --- 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. -- 2.39.2