- character: we adjusted some "autobatch" parameters

[helm.git] / helm / software / matita / contribs / limits / Domain / data.ma

diff --git a/helm/software/matita/contribs/limits/Domain/data.ma b/helm/software/matita/contribs/limits/Domain/data.ma
index f18e432798a3ff66c5b789c9f60f966c5d3d44f9..690b9483dd23a03782c8f6af8e44f5c810aca802 100644 (file)
--- 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.