From: Claudio Sacerdoti Coen 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.