1) PSig and Sig merged into a single Sigma type in Prop.

2) One function in list.ma that required the Sigma type in Type has been
   removed.

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 2a368527c635d0f463d6e2eb2a652b4a9fba0b77..40839b28fcf26fcf3abfe016fcb9b873a9ce19a1 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -121,12 +121,6 @@ lemma filter_false : ∀A,l,a,p. p a = false →
 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
-let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
-match l1 with
-  [ nil ⇒ nil ?
-  | cons a tl ⇒ (map ??(mk_Sig ?? a) (g a)) @ dprodl A f tl g
-  ].
-
 (**************************** length ******************************)
 
 let rec length (A:Type[0]) (l:list A) on l ≝ 

diff --git a/matita/matita/lib/basics/russell.ma b/matita/matita/lib/basics/russell.ma
index 059e024f9a4c9b73d7a711b60d7bab00082fba2a..71cc59fcd7e68ad0839e1993413b9d8e18e2dd15 100644 (file)
--- a/matita/matita/lib/basics/russell.ma
+++ b/matita/matita/lib/basics/russell.ma
@@ -12,5 +12,5 @@
 include "basics/jmeq.ma".
 include "basics/types.ma".
 
-coercion inject nocomposites: ∀A.∀P:A → Type[0].∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. mk_Sig … a p on a:? to Σx:?.?.
-coercion eject nocomposites: ∀A.∀P:A → Type[0].∀c:Σx:A.P x.A ≝ λA,P,c. pi1 … c on _c:Σx:?.? to ?.
+coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. mk_Sig … a p on a:? to Σx:?.?.
+coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ λA,P,c. pi1 … c on _c:Σx:?.? to ?.

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index a6749bb3991ac36427a53f4b0c04dd49706cf7ae..348bf92de73b52182447045a9efe08b9c590190b 100644 (file)
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -56,7 +56,7 @@ lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. 
 ] qed.
 
 (* sigma *)
-record Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
+record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
     pi1: A
   ; pi2: f pi1
   }.
@@ -123,12 +123,6 @@ notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
         λ${ident E}.$s ] (refl ? $t) }.
 
-(* Prop sigma *)
-record PSig (A:Type[0]) (P:A→Prop) : Type[0] ≝
-  {elem:>A; eproof: P elem}.
-  
-interpretation "subset type" 'sigma x = (PSig ? x).
-
 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
  with precedence 10
 for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒