From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jul 2009 12:36:46 +0000 (+0000)
Subject: More napply \ldots => napply
X-Git-Tag: make_still_working~3589
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=96881c08dcd617524621fb2f241fe38da81f2083;p=helm.git

More napply \ldots => napply
---

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index 40982a660..0f192e5f8 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -24,7 +24,7 @@ nrecord setoid : Type[1] ≝
  }.
 
 ndefinition proofs: CProp → setoid.
-#P; napply (mk_setoid …);
+#P; napply mk_setoid;
 ##[ napply P;
 ##| #x; #y; napply True;
 ##|##*: nwhd; nrepeat (#_); napply I;
@@ -39,11 +39,11 @@ nrecord function_space (A,B: setoid): Type ≝
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 
 ndefinition function_space_setoid: setoid → setoid → setoid.
- #A; #B; napply (mk_setoid …);
+ #A; #B; napply mk_setoid;
 ##[ napply (function_space A B);
 ##| #f; #f1; napply (∀a:A. proofs (eq … (f a) (f1 a)));
 ##| nwhd; #x; #a;
-    napply (f_ok … x …); (* QUI!! *)
+    napply (f_ok … x); (* QUI!! *)
 (*    unfold carr; unfold proofs; simplify;
     apply (refl A)
   | simplify;
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 3f5a4feee..eb99ee4c5 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -32,7 +32,7 @@ nqed.
 
 ntheorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
  #A; #S1; #S2; #S3; #H12; #H23; #x; #H;
- napply (H23 …); napply (H12 …); nassumption;
+ napply H23; napply H12; nassumption;
 nqed.
 
 ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.