X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fllt%2Fdefs.ma;h=7d5bc550aa23225d9e0e71a0a853396f9a7c733f;hb=3c6ff3987c3cc5e2df03fb76d07697c28c89c0a8;hp=96d869935859c7150fd6dab324fcb72f1987450e;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/llt/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/llt/defs.ma
index 96d869935..7d5bc550a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/llt/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/llt/defs.ma
@@ -14,14 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/A/defs.ma".
+include "basic_1/A/defs.ma".
 
-definition lweight:
- A \to nat
-\def
- let rec lweight (a: A) on a: nat \def (match a with [(ASort _ _) \Rightarrow 
-O | (AHead a1 a2) \Rightarrow (S (plus (lweight a1) (lweight a2)))]) in 
-lweight.
+rec definition lweight (a: A) on a: nat \def match a with [(ASort _ _) 
+\Rightarrow O | (AHead a1 a2) \Rightarrow (S (plus (lweight a1) (lweight 
+a2)))].
 
 definition llt:
  A \to (A \to Prop)