(* 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 domain built upon a subset *)
-definition domain_of_subset: \forall D. (Subset D) \to Domain \def
+(* the domain built upon a subset (not an implicit coercion) *)
+definition domain_of_subset: \forall D. Subset D \to Domain \def
\lambda (D:Domain). \lambda U.
mk_Domain (mk_Class D (sin D U) (cle1 D)).
-coercion domain_of_subset.
-
(* the full subset of a domain *)
coercion stop.