From 96881c08dcd617524621fb2f241fe38da81f2083 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jul 2009 12:36:46 +0000
Subject: [PATCH] More napply \ldots => napply

---
 helm/software/matita/nlibrary/sets/setoids.ma | 6 +++---
 helm/software/matita/nlibrary/sets/sets.ma    | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

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.
-- 
2.39.2