From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 13 Dec 2011 13:47:28 +0000 (+0000)
Subject: 1) PSig and Sig merged into a single Sigma type in Prop.
X-Git-Tag: make_still_working~2009
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=596896aaf7158f90a96c3220e4a8f0a420f593d6;p=helm.git

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 2a368527c..40839b28f 100644
--- 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 059e024f9..71cc59fcd 100644
--- 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 a6749bb39..348bf92de 100644
--- 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) ⇒