X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Flimits%2FDomain%2Fdata.ma;h=690b9483dd23a03782c8f6af8e44f5c810aca802;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=f18e432798a3ff66c5b789c9f60f966c5d3d44f9;hpb=700b170aa9b0377d33f1edd44de8d89129477fb8;p=helm.git

diff --git a/helm/software/matita/contribs/limits/Domain/data.ma b/helm/software/matita/contribs/limits/Domain/data.ma
index f18e43279..690b9483d 100644
--- a/helm/software/matita/contribs/limits/Domain/data.ma
+++ b/helm/software/matita/contribs/limits/Domain/data.ma
@@ -19,7 +19,9 @@ include "Domain/defs.ma".
 *)
 
 definition DBool: Domain ≝
-   mk_Domain (mk_Class bool (true_f ?) (eq ?)).
+   mk_Domain (
+      mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+   ).
 (*
 definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
    \lambda C,c0,c1,b.
@@ -29,7 +31,9 @@ definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
       ].
 *)
 definition DVoid: Domain ≝
-   mk_Domain (mk_Class void (true_f ?) (eq ?)).
+   mk_Domain (
+      mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+   ).
 (*
 definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def
    \lambda C,v.