Removed final question marks from {apply|elim|rewrite}s.

[helm.git] / helm / matita / library / Q / q.ma

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index 4878078fc44482f8ed80b3d138c27d7ba9446726..1ff2adcd8dfa0bf99462486ce3641519849e0df7 100644 (file)
--- 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.