Parentheses must now be put in patterns like in tactic arguments.

diff --git a/helm/matita/contribs/LAMBDA-TYPES/.depend b/helm/matita/contribs/LAMBDA-TYPES/.depend
index dd2c59b7554e7afe42448732188341cad493dc23..b4b21a2e6e2fbade0c26ff1a5aa8ccef4476f1c7 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/.depend
+++ b/helm/matita/contribs/LAMBDA-TYPES/.depend
@@ -1,9 +1,9 @@
-/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo: ./lref_map_defs.ma /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
-./lref_map_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo
-/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo: ./terms_defs.ma /home/tassi/helm/matita/coq.moo
-./terms_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
-/home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo: ./tlt_defs.ma /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
-./tlt_defs.mo: /home/tassi/helm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo
+/home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo: ./lref_map_defs.ma /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
+./lref_map_defs.mo: /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/lref_map_defs.moo
+/home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo: ./terms_defs.ma /home/sacerdot/miohelm/matita/coq.moo
+./terms_defs.mo: /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
+/home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo: ./tlt_defs.ma /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/terms_defs.moo
+./tlt_defs.mo: /home/sacerdot/miohelm/matita/.matita/xml/matita/LAMBDA-TYPES/tlt_defs.moo
 !! TOTAL TIME SPENT IN disambiguate_thing: 0.
 !! TOTAL TIME SPENT IN disambiguate_thing.refine_thing: 0.
 !! TOTAL TIME SPENT IN add_obj: 0.

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 19158e300bec21656616171ff60a1052c4007ec7..27266bf393c41e5457f5cd6723bb8276035df5c6 100644 (file)
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -148,8 +148,8 @@ lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q). 
 intros.
 simplify. 
-change in match p + n * (S p) with (pred ((S n) * (S p))).
-change in match q + n * (S q) with (pred ((S n) * (S q))).
+change in match (p + n * (S p)) with (pred ((S n) * (S p))).
+change in match (q + n * (S q)) with (pred ((S n) * (S q))).
 rewrite < nat_compare_pred_pred.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.

diff --git a/helm/matita/tests/change.ma b/helm/matita/tests/change.ma
index 511754d2743ee6af31b939298a9082a8883e43cf..16b6753167000a94134e3a1b32c7b2c4014f04a2 100644 (file)
--- a/helm/matita/tests/change.ma
+++ b/helm/matita/tests/change.ma
@@ -33,8 +33,8 @@ qed.
 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
 theorem t: (\forall x:nat. x=x) \to True.
  intro H.
- change in match x in H : \forall _.% with (0+x).
- change in H: \forall _.(? ? ? (? % ?)) with 0.
+ change in match x in H : (\forall _.%) with (0+x).
+ change in H: (\forall _.(? ? ? (? % ?))) with 0.
  constructor 1.
 qed.
 

diff --git a/helm/matita/tests/replace.ma b/helm/matita/tests/replace.ma
index 8504b6c160c78eb5298c5d276fa3cc80b2109933..b5d1eb355514bec21c75b0775e3bfffd01c82b8e 100644 (file)
--- a/helm/matita/tests/replace.ma
+++ b/helm/matita/tests/replace.ma
@@ -35,5 +35,5 @@ qed.
 
 (* This test tests "replace in match t" where t contains some metavariables *)
 theorem t2: 2 + (3 * 4) = (5 + 5) + 2 * 2.
- replace in match 5+? with (6 + 4); [reflexivity | reflexivity].
+ replace in match (5+?) with (6 + 4); [reflexivity | reflexivity].
 qed.

diff --git a/helm/matita/tests/unfold.ma b/helm/matita/tests/unfold.ma
index d63dd50d46d8a6a8027234ff691815f4a71c537b..d17e5a2daf9fd243c136f10cfcd6997707226ede 100644 (file)
--- a/helm/matita/tests/unfold.ma
+++ b/helm/matita/tests/unfold.ma
@@ -19,12 +19,13 @@ include "coq.ma".
 alias symbol "plus" (instance 0) = "Coq's natural plus".
 definition myplus \def \lambda x,y. x+y.
 
+alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
 lemma lem: \forall n. S (n + n) = (S n) + n.
  intro; reflexivity.
 qed.
 
 theorem trivial: \forall n. S (myplus n n) = myplus (S n) n.
- unfold myplus in \vdash \forall _.(? ? ? %).
+ unfold myplus in \vdash (\forall _.(? ? ? %)).
  intro.
  unfold myplus.
  rewrite > lem.
@@ -33,6 +34,7 @@ qed.
 
 (* This test needs to parse "uno" in the context of the hypothesis H,
    not in the context of the goal. *)
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
 theorem t: let uno \def S O in uno + uno = S uno \to uno=uno.
  intros. unfold uno in H.
  reflexivity.