More napply \ldots => napply

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index 40982a660438b3479e40d5502aba581041d2ec47..0f192e5f8ee780f436fcc9553d8761852bb2ddae 100644 (file)
--- 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 3f5a4feeeceb634c199b7b7c8727c3289f729025..eb99ee4c5c22595075b5dae056155cacb7d856ca 100644 (file)
--- 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.