"Coq's " prefix added to every interpretation.

diff --git a/helm/matita/tests/absurd.ma b/helm/matita/tests/absurd.ma
index f5f27f6229dcc0617bada233837ffdbc5693d8d6..24d2d885f945198023f1bbbcafd53d829aa14aaa 100644 (file)
--- a/helm/matita/tests/absurd.ma
+++ b/helm/matita/tests/absurd.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/tests/absurd/".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+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 0fcf73cf32fc81cbf60dc44c4549116e69df5ec9..41bdd3afc63e19fec85e78d8137967dbd36ce871 100644 (file)
--- a/helm/matita/tests/apply.ma
+++ b/helm/matita/tests/apply.ma
@@ -14,7 +14,7 @@ qed.
 
 (* test _without_ the WHD on the apply argument *)
 
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 
 theorem a:
   \forall A:Set.

diff --git a/helm/matita/tests/assumption.ma b/helm/matita/tests/assumption.ma
index 711e35cf00278f97949166f41e09c6441f6771ae..4679ea1c32e5d414cc1f38799385524a908e1adc 100644 (file)
--- a/helm/matita/tests/assumption.ma
+++ b/helm/matita/tests/assumption.ma
@@ -16,9 +16,9 @@ set "baseuri" "cic:/matita/tests/assumption".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias num (instance 0) = "natural number".
-alias symbol "and" (instance 0) = "logical and".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "plus" (instance 0) = "natural plus".
+alias symbol "and" (instance 0) = "Coq's logical and".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "plus" (instance 0) = "Coq's natural plus".
 
 
 theorem stupid:

diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma
index 66b973cfd5b27197fbba6fa681570492109d3fb0..e7e59554c3764b1f3c226ba040603b7f49453a39 100755 (executable)
--- a/helm/matita/tests/auto.ma
+++ b/helm/matita/tests/auto.ma
@@ -3,10 +3,10 @@ set "baseuri" "cic:/matita/tests/auto/".
 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)".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "minus" (instance 0) = "natural minus".
-alias symbol "plus" (instance 0) = "natural plus".
-alias symbol "times" (instance 0) = "natural times".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "minus" (instance 0) = "Coq's natural minus".
+alias symbol "plus" (instance 0) = "Coq's natural plus".
+alias symbol "times" (instance 0) = "Coq's natural times".
 theorem a : \forall x,y:nat. x*x+(S y) = O - x.
 intros.
 auto depth = 3.

diff --git a/helm/matita/tests/change.ma b/helm/matita/tests/change.ma
index ea894c28e2aacb3726fcc8c4f2ee8dbbd52e4f6c..199ce3bd8352c8eb2b6d3954b74efef06d89bbe7 100644 (file)
--- a/helm/matita/tests/change.ma
+++ b/helm/matita/tests/change.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/tests/change/".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "plus" (instance 0) = "natural plus".
+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)".
 
 theorem stupid: 
@@ -26,4 +26,4 @@ intros.
 change in \vdash (? ? % ?) with 5.
 rewrite < H in \vdash (? ? % ?). 
 reflexivity.
-qed.
\ No newline at end of file
+qed.

diff --git a/helm/matita/tests/clear.ma b/helm/matita/tests/clear.ma
index 1fe721d59db385a3ee299a34ad3f6b522ed04447..24bb3377ca92172c0f2653848677f9c5776529f2 100644 (file)
--- a/helm/matita/tests/clear.ma
+++ b/helm/matita/tests/clear.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/tests/clear".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+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 29dd2457dae94317c6561786c206d2bb07743e51..9a125e687530a041aaab0b2dad6b57d636f97c4e 100644 (file)
--- a/helm/matita/tests/clearbody.ma
+++ b/helm/matita/tests/clearbody.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/tests/clearbody".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "plus" (instance 0) = "natural plus".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "plus" (instance 0) = "Coq's natural plus".
 
 
 theorem stupid : 

diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma
index 2444b1d74a3a638dddb85a3b42cf84d11acf6a82..5c157368d053b4a708ee84f43bc211e996653b41 100644 (file)
--- a/helm/matita/tests/coercions.ma
+++ b/helm/matita/tests/coercions.ma
@@ -26,7 +26,7 @@ coercion pos2nat.
 coercion nat2int.
 
 definition fst \def \lambda x,y:int.x.
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 
 theorem a: fst O one = fst (positive O) (next one).
 reflexivity.

diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma
index cd21535e7213a671e1a0307aa5bc8cc8d91a2d5e..e9caa7edc183a5922178343ad10d4c1e9ad91218 100644 (file)
--- a/helm/matita/tests/comments.ma
+++ b/helm/matita/tests/comments.ma
@@ -19,7 +19,7 @@ set "baseuri" "cic:/matita/tests/comments/".
 *)
 
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 theorem a:0=0.
 
 (* nota *)

diff --git a/helm/matita/tests/constructor.ma b/helm/matita/tests/constructor.ma
index 5f9bed6c01dcb9cd39a0a82e12502d02a80f234e..0cd22d35bc1d53c4fd42402afce9175da4cead8b 100644 (file)
--- a/helm/matita/tests/constructor.ma
+++ b/helm/matita/tests/constructor.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/tests/constructor".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 
 
 theorem stupid: 1 = 1.

diff --git a/helm/matita/tests/contradiction.ma b/helm/matita/tests/contradiction.ma
index d5199aefc1ce02c563a3eb2fc748bde0138f8add..e4519ec3e10b8a2217020e444112030e92cee7ae 100644 (file)
--- a/helm/matita/tests/contradiction.ma
+++ b/helm/matita/tests/contradiction.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/tests/contradiction".
 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".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 
 
 

diff --git a/helm/matita/tests/cut.ma b/helm/matita/tests/cut.ma
index 82d36667b6d6daffa900f638eb3d856530a02cb5..f5850e576589a664c81742d11c15df68b063e753 100644 (file)
--- a/helm/matita/tests/cut.ma
+++ b/helm/matita/tests/cut.ma
@@ -14,11 +14,11 @@
 
 set "baseuri" "cic:/matita/tests/cut".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 
 theorem stupid: 3 = 3.
   cut 3 = 3.
   assumption.
   reflexivity.
   qed.
-  
\ No newline at end of file
+  

diff --git a/helm/matita/tests/decompose.ma b/helm/matita/tests/decompose.ma
index 48477f3ebf4851a8fcedb75d38d1b4568aad26fe..0b5ef7a804d3c6c76c23a43f8a495ee27d9c5efa 100644 (file)
--- a/helm/matita/tests/decompose.ma
+++ b/helm/matita/tests/decompose.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/decompose".
-alias symbol "and" (instance 0) = "logical and".
-alias symbol "or" (instance 0) = "logical or".
+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 ca55591ee88c7366dc61bc9c632dea5e26cfb078..f94624567c75c028be737c655b3a88a3b8839aa3 100644 (file)
--- a/helm/matita/tests/discriminate.ma
+++ b/helm/matita/tests/discriminate.ma
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/tests/discriminate".
 alias id "not" = "cic:/Coq/Init/Logic/not.con".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 
 
 theorem stupid:

diff --git a/helm/matita/tests/elim.ma b/helm/matita/tests/elim.ma
index cf4e1eb22301551cbdb510c5d91eef59a6b091c4..ab7afafa69e34cf52a33b9530ffaa2aa4e5ab9b6 100644 (file)
--- a/helm/matita/tests/elim.ma
+++ b/helm/matita/tests/elim.ma
@@ -19,9 +19,9 @@ inductive stupidtype: Set \def
   | Next : stupidtype \to stupidtype
   | Pair : stupidtype \to stupidtype \to stupidtype.
   
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "exists" (instance 0) = "exists".
-alias symbol "or" (instance 0) = "logical or".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "exists" (instance 0) = "Coq's exists".
+alias symbol "or" (instance 0) = "Coq's logical or".
 alias num (instance 0) = "natural number".
 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".

diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index bfd24e5910e462bfadfd4a970ea4f37e31d8d6e8..07e7989ceb38745e55dca3d61b0a9556f0cd180f 100644 (file)
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -10,9 +10,9 @@ alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
 
-alias symbol "and" (instance 0) = "logical and".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "exists" (instance 0) = "exists".
+alias symbol "and" (instance 0) = "Coq's logical and".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "exists" (instance 0) = "Coq's exists".
 
 definition is_S: nat \to Prop \def
    \lambda n. match n with 

diff --git a/helm/matita/tests/fold.ma b/helm/matita/tests/fold.ma
index f2f26a849c8e66f0c662af5d0d2f52842ee82a0d..7b91c5b24036c30eb2e6aae0c05b383dd52cef79 100644 (file)
--- a/helm/matita/tests/fold.ma
+++ b/helm/matita/tests/fold.ma
@@ -1,8 +1,8 @@
 set "baseuri" "cic:/matita/tests/fold".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "plus" (instance 0) = "natural plus".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "plus" (instance 0) = "Coq's natural plus".
 theorem t: \forall x:nat. 0+x=x.
  intro.
  simplify in match (0+x) in \vdash (? ? % ?).

diff --git a/helm/matita/tests/generalize.ma b/helm/matita/tests/generalize.ma
index a6e56ef3e06215863ec94c73b73b209d806af2eb..4fe9af34067132f04431b03de8a47b37baf9ea70 100644 (file)
--- a/helm/matita/tests/generalize.ma
+++ b/helm/matita/tests/generalize.ma
@@ -15,8 +15,8 @@
 set "baseuri" "cic:/matita/generalize".
 
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "plus" (instance 0) = "natural plus".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "plus" (instance 0) = "Coq's natural plus".
 alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
 
@@ -33,4 +33,4 @@ qed.
 theorem test2: \forall x. x + 4 = 4 + x.
  generalize in match 4.
  exact plus_comm.
-qed.
\ No newline at end of file
+qed.

diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
index c76851f59fa8dd1240d87fdb04d8072a5544ba5f..99e18012d79bdc43ac445116627aefcf26eef832 100644 (file)
--- a/helm/matita/tests/inversion.ma
+++ b/helm/matita/tests/inversion.ma
@@ -8,7 +8,7 @@ inductive le (n:nat) : nat \to Prop \def
    leO : le n n
  | leS : \forall m. le n m \to le n (S m).
 
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 
 theorem test_inversion: \forall n. le n O \to n=O.
  intros.

diff --git a/helm/matita/tests/paramodulation.ma b/helm/matita/tests/paramodulation.ma
index b56c0da27d1672cf11046bb0bee882048c8997b3..80a39fa3f141a567733cbe93d535e895b997ce77 100644 (file)
--- a/helm/matita/tests/paramodulation.ma
+++ b/helm/matita/tests/paramodulation.ma
@@ -14,10 +14,10 @@
 
 set "baseuri" "cic:/matita/tests/paramodulation".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "plus" (instance 0) = "natural plus".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias symbol "plus" (instance 0) = "Coq's natural plus".
 alias num (instance 0) = "natural number".
-alias symbol "times" (instance 0) = "natural times".
+alias symbol "times" (instance 0) = "Coq's natural times".
 
 theorem para1:
   \forall n,m,n1,m1:nat.

diff --git a/helm/matita/tests/replace.ma b/helm/matita/tests/replace.ma
index d209e97d42f6fb6ea474d5dcfc8486a0943ecf01..d70a7af600a7c08909f87f2e2683cef65ad44e5e 100644 (file)
--- a/helm/matita/tests/replace.ma
+++ b/helm/matita/tests/replace.ma
@@ -1,9 +1,9 @@
 set "baseuri" "cic:/matita/tests/replace/".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
-alias symbol "plus" (instance 0) = "natural plus".
-alias symbol "times" (instance 0) = "natural times".
+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".
 alias id "mult_n_O" = "cic:/Coq/Init/Peano/mult_n_O.con".
 alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
 

diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma
index aa4fa1f3285ad09f7cb64ce287cda697680b3881..71a7514fa1f519e5b4c1f085d3b34db31e4393a8 100644 (file)
--- a/helm/matita/tests/rewrite.ma
+++ b/helm/matita/tests/rewrite.ma
@@ -2,8 +2,8 @@ set "baseuri" "cic:/matita/tests/rewrite/".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality". 
-alias symbol "plus" (instance 0) = "natural plus".
+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".
 
 theorem a:
@@ -31,4 +31,4 @@ qed.
 theorem foo: \forall n. n = n + 0.
  intros.
  rewrite < t; reflexivity.
-qed.
\ No newline at end of file
+qed.

diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
index 3edc4cf35f986d54bd1ed36c02e5ab11f644091b..61d5b11631451266bfdfebc87634f0ca5c4d86b3 100644 (file)
--- a/helm/matita/tests/simpl.ma
+++ b/helm/matita/tests/simpl.ma
@@ -1,7 +1,7 @@
 set "baseuri" "cic:/matita/tests/simpl/".
 
 alias id "not" = "cic:/Coq/Init/Logic/not.con".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 theorem a : 
  \forall A:Set.
  \forall x,y : A.

diff --git a/helm/matita/tests/test2.ma b/helm/matita/tests/test2.ma
index cf265671072179f73e309c9ecba6a36a0b78bfb0..1adf17326007cf5276d32dbfc231dbda79aa1d5a 100644 (file)
--- a/helm/matita/tests/test2.ma
+++ b/helm/matita/tests/test2.ma
@@ -1,8 +1,8 @@
 set "baseuri" "cic:/matita/tests/test2/".
 
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias symbol "and" (instance 0) = "logical and".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "and" (instance 0) = "Coq's logical and".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 theorem a:\forall x:nat.x=x\land x=x.
 intro.
 split.

diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma
index 9a8958b2175360f26ab23ddadf7adad908725261..561bd6564bad0ca0e8da9bcf936c7c70e141c2ce 100644 (file)
--- a/helm/matita/tests/test3.ma
+++ b/helm/matita/tests/test3.ma
@@ -1,6 +1,6 @@
 set "baseuri" "cic:/matita/tests/test3/".
 
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 theorem a:\forall x.x=x.
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 exact nat.
@@ -8,7 +8,7 @@ intro.
 reflexivity.
 qed.
 alias num (instance 0) = "natural number".
-alias symbol "times" (instance 0) = "natural times".
+alias symbol "times" (instance 0) = "Coq's natural times".
 
 theorem b:\forall p:nat. p * 0=0.
 intro.

diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma
index be67f3a8eacd5793e4c124b21935125b3a3600fa..8d8cac4e3653bfba8c258ce2d43bf4187f896676 100644 (file)
--- a/helm/matita/tests/test4.ma
+++ b/helm/matita/tests/test4.ma
@@ -6,7 +6,7 @@ set "baseuri" "cic:/matita/tests/test4/".
 *)
 
 alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
 theorem a:0=0.
 
 (* nota *)