From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Sep 2005 09:41:19 +0000 (+0000)
Subject: Removed final question marks from {apply|elim|rewrite}s.
X-Git-Tag: LAST_BEFORE_NEW~105
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8c6dd0220fba9ebed2d51d5808790b5949177ea;p=helm.git

Removed final question marks from {apply|elim|rewrite}s.
(This used to change the goals order, but it has now been fixed by Gares)
---

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index 4878078fc..1ff2adcd8 100644
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -162,13 +162,13 @@ apply fraction_elim2 (\lambda f,g. Or (f=g) (f=g \to False)).
     right.apply not_eq_pp_nn.
     right.apply not_eq_pp_cons.
   intros. elim g1.
-      right.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
+      right.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
       elim ((decidable_eq_nat n n1) : Or (n=n1) (n=n1 \to False)).
         left. apply eq_f. assumption.
         right.intro.apply H.apply injective_nn.assumption.
       right.apply not_eq_nn_cons.
-  intros.right.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq.assumption.
-  intros.right.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq.assumption.
+  intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
+  intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.
   intros.elim H.
     elim ((decidable_eq_Z x y) : Or (x=y) (x=y \to False)).
       left.apply eq_f2.assumption.
@@ -192,12 +192,12 @@ intros.apply fraction_elim2
     simplify.apply not_eq_pp_nn.
     simplify.apply not_eq_pp_cons.
   intros.elim g1.
-    simplify.intro.apply not_eq_pp_nn n1 n ?.apply sym_eq. assumption.
+    simplify.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
     intro.simplify.intro.apply H.apply injective_nn.assumption.
   simplify.apply not_eq_nn_cons.
-  intros.simplify.intro.apply not_eq_pp_cons m x f1 ?.apply sym_eq. assumption.
-  intros.simplify.intro.apply not_eq_nn_cons m x f1 ?.apply sym_eq. assumption.
+  intros.simplify.intro.apply not_eq_pp_cons m x f1.apply sym_eq. assumption.
+  intros.simplify.intro.apply not_eq_nn_cons m x f1.apply sym_eq. assumption.
   intros.
    change in match (eqfb (cons x f1) (cons y g1)) 
    with (andb (eqZb x y) (eqfb f1 g1)).
@@ -317,4 +317,4 @@ theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.
 intro.elim r.
 reflexivity.
 simplify.apply ftimes_finv.
-qed.
\ No newline at end of file
+qed.
diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index dc743e60b..b89f291fb 100644
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -59,12 +59,12 @@ simplify.
 rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 simplify.
 rewrite > nat_compare_n_m_m_n.
-simplify.elim nat_compare ? ?.simplify.reflexivity.
+simplify.elim nat_compare.simplify.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
 elim y.simplify.reflexivity.
 simplify.rewrite > nat_compare_n_m_m_n.
-simplify.elim nat_compare ? ?.simplify.reflexivity.
+simplify.elim nat_compare.simplify.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
 simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index c4e965fbf..a36bd078c 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -78,24 +78,24 @@ intros.elim x.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
         apply lt_O_times_S_S.apply lt_O_times_S_S.
   elim y.
     simplify.reflexivity.
@@ -104,24 +104,24 @@ intros.elim x.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
 qed.
 
@@ -134,8 +134,8 @@ eq nat (times (S n) (S (pred (minus (S p) (S q)))))
        (minus (pred (times (S n) (S p))) 
               (pred (times (S n) (S q)))).
 intros.
-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
+rewrite < S_pred.  
+rewrite > minus_pred_pred.
 rewrite < distr_times_minus. 
 reflexivity.  
 (* we now close all positivity conditions *)
@@ -151,7 +151,7 @@ intros.
 simplify. 
 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
-rewrite < nat_compare_pred_pred ? ? ? ?.
+rewrite < nat_compare_pred_pred.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.
 apply nat_compare_elim p q.
@@ -236,4 +236,4 @@ qed.
 
 variant distr_Ztimes_Zplus: \forall x,y,z.
 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
-distributive_Ztimes_Zplus.
\ No newline at end of file
+distributive_Ztimes_Zplus.
diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 443c6657f..22c8b25a7 100644
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -43,7 +43,7 @@ simplify.reflexivity.
 simplify.apply not_eq_O_S.
 intro.
 simplify.
-intro. apply not_eq_O_S n1 ?.apply sym_eq.assumption.
+intro. apply not_eq_O_S n1.apply sym_eq.assumption.
 intros.simplify.
 generalize in match H.
 elim (eqb n1 m1).
diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index ede15596a..ad74a324d 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -126,7 +126,7 @@ cut b \leq (q1-q)*b+r1.
 cut b \leq r.
 apply lt_to_not_le r b H2 Hcut2.
 elim Hcut.assumption.
-apply trans_le ? ((q1-q)*b) ?.
+apply trans_le ? ((q1-q)*b).
 apply le_times_n.
 apply le_SO_minus.exact H6.
 rewrite < sym_plus.
@@ -134,7 +134,7 @@ apply le_plus_n.
 rewrite < sym_times.
 rewrite > distr_times_minus.
 (* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *)
-rewrite > plus_minus ? ? ? ?.
+rewrite > plus_minus.
 rewrite > sym_times.
 rewrite < H5.
 rewrite < sym_times.
@@ -154,14 +154,14 @@ cut b \leq (q-q1)*b+r.
 cut b \leq r1.
 apply lt_to_not_le r1 b H4 Hcut2.
 elim Hcut.assumption.
-apply trans_le ? ((q-q1)*b) ?.
+apply trans_le ? ((q-q1)*b).
 apply le_times_n.
 apply le_SO_minus.exact H6.
 rewrite < sym_plus.
 apply le_plus_n.
 rewrite < sym_times.
 rewrite > distr_times_minus.
-rewrite > plus_minus ? ? ? ?.
+rewrite > plus_minus.
 rewrite > sym_times.
 rewrite < H3.
 rewrite < sym_times.
@@ -275,4 +275,4 @@ apply inj_times_l m.assumption.
 qed.
 
 variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
-\def lt_O_to_injective_times_l.
\ No newline at end of file
+\def lt_O_to_injective_times_l.
diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index a3a715228..4628eca13 100644
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -216,7 +216,7 @@ elim Hcut2.absurd O=r.
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
 simplify.intro.
 cut O=n1.
-apply not_le_Sn_O O ?.
+apply not_le_Sn_O O.
 rewrite > Hcut3 in \vdash (? ? %).
 assumption.rewrite > Hcut. 
 rewrite < H6.reflexivity.
@@ -273,7 +273,7 @@ cut (S(S m1)) = r.
 rewrite > Hcut3 in \vdash (? (? ? %)).
 change with divides (nth_prime p) r \to False.
 intro.
-apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r ? ? ? ?.
+apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r.
 apply lt_SO_nth_prime_n.
 simplify.apply le_S_S.apply le_O_n.apply le_n.
 assumption.
@@ -301,7 +301,7 @@ cut r \lt (S O) \or r=(S O).
 elim Hcut3.absurd O=r.
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
 simplify.intro.
-apply not_le_Sn_O O ?.
+apply not_le_Sn_O O.
 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply le_to_or_lt_eq r (S O).
 apply not_lt_to_le.assumption.
@@ -400,7 +400,7 @@ intro.
 cut i = j.
 apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply injective_nth_prime ? ? H4.
-apply H i (S j) ?.
+apply H i (S j).
 apply trans_lt ? j.assumption.simplify.apply le_n.
 assumption.
 apply divides_times_to_divides.
@@ -470,7 +470,7 @@ simplify in H4.
 rewrite > plus_n_O.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption.
 apply False_ind.
-apply not_divides_defactorize_aux n1 i (S i) ?.
+apply not_divides_defactorize_aux n1 i (S i).
 simplify. apply le_n.
 simplify in H5.
 rewrite > plus_n_O (defactorize_aux n1 (S i)).
@@ -480,7 +480,7 @@ apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))).
 reflexivity.
 intros.
 apply False_ind.
-apply not_divides_defactorize_aux n3 i (S i) ?.
+apply not_divides_defactorize_aux n3 i (S i).
 simplify. apply le_n.
 simplify in H4.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).
diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma
index 301c0be8e..3babb5c75 100644
--- a/helm/matita/library/nat/log.ma
+++ b/helm/matita/library/nat/log.ma
@@ -178,7 +178,7 @@ rewrite > H4.
 (* META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.
-apply not_eq_O_S m1 ?.
+apply not_eq_O_S m1.
 rewrite > H5.reflexivity.
 qed.
 
diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma
index 748399fbc..4dfda0ba6 100644
--- a/helm/matita/library/nat/minimization.ma
+++ b/helm/matita/library/nat/minimization.ma
@@ -86,7 +86,7 @@ simplify.
 apply bool_ind (\lambda b:bool.
 (f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
 [ true \Rightarrow (S n1)
-| false  \Rightarrow (max n1 f)])) = true) ? ? ?.
+| false  \Rightarrow (max n1 f)])) = true).
 simplify.intro.assumption.
 simplify.intro.apply H.
 elim H1.elim H3.generalize in match H5.
@@ -94,7 +94,7 @@ apply le_n_Sm_elim a n1 H4.
 intros.
 apply ex_intro nat ? a.
 split.apply le_S_S_to_le.assumption.assumption.
-intros.apply False_ind.apply not_eq_true_false ?.
+intros.apply False_ind.apply not_eq_true_false.
 rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
 reflexivity.
 qed.
@@ -163,7 +163,7 @@ simplify.
 apply bool_ind (\lambda b:bool.
 (f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
 [ true \Rightarrow m-(S n)
-| false  \Rightarrow (min_aux n m f)])) = true) ? ? ?.
+| false  \Rightarrow (min_aux n m f)])) = true).
 simplify.intro.assumption.
 simplify.intro.apply H.
 elim H1.elim H3.elim H4.
@@ -204,7 +204,7 @@ rewrite > min_aux_O_f f n.apply le_n.
 elim min_aux_S f n1 n.
 elim H1.rewrite > H3.apply le_n.
 elim H1.rewrite > H3.
-apply trans_le (n-(S n1)) (n-n1) ?.
+apply trans_le (n-(S n1)) (n-n1).
 apply monotonic_le_minus_r.
 apply le_n_Sn.
 assumption.
diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 3acce20af..079e902ad 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -82,7 +82,7 @@ qed.
 
 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
 n = m+p.
-intros.apply trans_eq ? ? ((n-m)+m) ?.
+intros.apply trans_eq ? ? ((n-m)+m).
 apply plus_minus_m_m.
 apply H.elim H1.
 apply sym_plus.
@@ -220,7 +220,7 @@ apply (leb_elim z y).
     apply inj_plus_l (x*z).assumption.
     apply trans_eq nat ? (x*y).
       rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
-      rewrite < plus_minus_m_m ? ? ?.
+      rewrite < plus_minus_m_m.
         reflexivity.
         apply le_times_r.assumption.
   intro.rewrite > eq_minus_n_m_O.
diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index 100cb0f03..aae6434e7 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -97,7 +97,7 @@ intro.elim n1.
 left.reflexivity.
 right.apply not_eq_O_S.
 intro.right.intro.
-apply not_eq_O_S n1 ?.
+apply not_eq_O_S n1.
 apply sym_eq.assumption.
 intros.elim H.
 left.apply eq_f. assumption.
diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 37c60b405..0b8f2bbe2 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -43,7 +43,7 @@ n < smallest_factor (S (fact n)).
 intros.
 apply not_le_to_lt.
 change with smallest_factor (S (fact n)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
+apply not_divides_S_fact n (smallest_factor(S (fact n))).
 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.