- external quantification removed (will be reintroduced when needed)

[helm.git] / helm / software / matita / contribs / limits / Subset / defs.ma

diff --git a/helm/software/matita/contribs/limits/Subset/defs.ma b/helm/software/matita/contribs/limits/Subset/defs.ma
index ed5c8a47ee77abd6433d3bb07af5a8be0c903545..6dbab4b39de63ed4fceed84f9ee07f5ac5fa63ac 100644 (file)
--- a/helm/software/matita/contribs/limits/Subset/defs.ma
+++ b/helm/software/matita/contribs/limits/Subset/defs.ma
@@ -28,6 +28,8 @@ definition sin : ∀D. Subset D → D → Prop ≝
 (* subset top (full subset) *)
 definition stop ≝ λD:Domain. true_f D.
 
+coercion stop.
+
 (* subset bottom (empty subset) *)
 definition sbot ≝ λD:Domain. false_f D.
 
@@ -47,17 +49,10 @@ definition sle: ∀D. Subset D → Subset D → Prop ≝
 definition sover: ∀D. Subset D → Subset D → Prop ≝
    λD,U1,U2. \iexists d. U1 d ∧ U2 d. 
 
-(* coercions **************************************************************)
-
-(*
-(* the class of the subsets of a domain (not an implicit coercion) *)
-definition class_of_subsets_of \def
-   \lambda D. mk_Class (Subset D) (true_f ?) (sle ?). 
-*)
+(* the class of the subsets of a domain *)
+definition subsets_of_domain ≝
+   λD. mk_Class (Subset D) (true_f ?) (sle ?). 
 
-(* the domain built upon a subset (not an implicit coercion) *)
-definition domain_of_subset: ∀D. Subset D \to Domain ≝
+(* the domain built upon a subset *)
+definition domain_of_subset: ∀D. Subset D → Domain ≝
    λD:Domain. λU. mk_Domain (mk_Class D (sin D U) (ces D)).
-
-(* the full subset of a domain *)
-coercion stop.