new makefiles

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / tau0 / defs.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/defs.ma
index 14373ffcd2a2e0c158127629541a7d26e6c2c49a..84f1a28ca1bb29e3914d49c3f21e72574bd61e05 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/defs.ma
@@ -20,7 +20,7 @@ include "G/defs.ma".
 
 include "getl/defs.ma".
 
-inductive tau0 (g:G): C \to (T \to (T \to Prop)) \def
+inductive tau0 (g: G): C \to (T \to (T \to Prop)) \def
 | tau0_sort: \forall (c: C).(\forall (n: nat).(tau0 g c (TSort n) (TSort 
 (next g n))))
 | tau0_abbr: \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: