napply now automatically inserts \ldots at the end

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 445ac030e7674e758998ac74543a84162b05e991..b2a48c6fdcb9b1781b936ba12a9d947266d0079a 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -434,7 +434,7 @@ let letin_tac ~where ~what:(_,_,w) name =
  ]
 ;;
 
-let apply_tac = exact_tac;;
+let apply_tac (s,n,t) = exact_tac (s,n,Ast.Appl [t; Ast.Implicit `Vector]);;
 
 type indtyinfo = {
         rightno: int;

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 74663f45a58335f8498267e41e3bfd2fa31cfe68..2366e0fc67a6e0431a38389901bc9e2da23b45bc 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -40,16 +40,16 @@ ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
 ndefinition mm_image:
  ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma B.
  #A; #B; #Ma; #Mb; #f;
- napply (mk_magma …)
+ napply mk_magma
   [ napply (image … f Ma)
   | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
-    napply (ex_intro …)
+    napply ex_intro
      [ napply (op … x0 y0) 
-     | napply (conj …)
-        [ napply (op_closed …); nassumption
+     | napply conj
+        [ napply op_closed; nassumption
         | nrewrite < Hx1;
           nrewrite < Hy1;
-          napply (mmprop … f …)]##]
+          napply (mmprop … f)]##]
 nqed.
 
 ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
@@ -58,16 +58,16 @@ ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
 ndefinition mm_counter_image:
  ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma A.
   #A; #B; #Ma; #Mb; #f;
-  napply (mk_magma …)
+  napply mk_magma
    [ napply (counter_image … f Mb)
    | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
-     napply (ex_intro …)
+     napply ex_intro
       [ napply (op … x0 y0)
-      | napply (conj …)
-         [ napply (op_closed …); nassumption
+      | napply conj
+         [ napply op_closed; nassumption
          | nrewrite < Hx1;
            nrewrite < Hy1;
-           napply (mmprop … f …)]##]
+           napply (mmprop … f)]##]
 nqed.
 
 ndefinition m_intersect: ∀A. magma A → magma A → magma A.
@@ -75,5 +75,5 @@ ndefinition m_intersect: ∀A. magma A → magma A → magma A.
  napply (mk_magma …)
   [ napply (M1 ∩ M2)
   | #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
-    napply (conj …); napply (op_closed …); nassumption ]
+    napply conj; napply op_closed; nassumption ]
 nqed.
\ No newline at end of file