some corrections and additions

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma
index ced0a2668d9a6ae628bf4373380379740206194d..559bf5da7100c1be3270ec565d4ad88dda94fb6b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma
@@ -14,9 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-
-
-include "tau0/defs.ma".
+include "LambdaDelta-1/tau0/defs.ma".
 
 inductive tau1 (g: G) (c: C) (t1: T): T \to Prop \def
 | tau1_tau0: \forall (t2: T).((tau0 g c t1 t2) \to (tau1 g c t1 t2))