From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 25 Oct 2005 16:46:04 +0000 (+0000)
Subject: Parentheses must now be put in patterns like in tactic arguments.
X-Git-Tag: V_0_7_2_3~183
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10191b6a5e928b355cd1244b7dd15533ebf52924;p=helm.git

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 dd2c59b75..b4b21a2e6 100644
--- 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 19158e300..27266bf39 100644
--- 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 511754d27..16b675316 100644
--- 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 8504b6c16..b5d1eb355 100644
--- 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 d63dd50d4..d17e5a2da 100644
--- 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.