ocaml 3.09 transition

[helm.git] / helm / matita / contribs / LAMBDA-TYPES / tlt_defs.ma

diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
index 1d5f73f17b01283028da43a233572ae7e6c6bb46..390c067cc15823721e09fdf7f81653f2f1e2a9c1 100644 (file)
--- a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma
@@ -44,6 +44,10 @@ let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T A N) on t : nat \def
       | (TGRef y n)     \Rightarrow O
   ].
 
-definition weight : \forall A,N. T A N \to nat \def \lambda A,N.(weight_map A N (\lambda _.O)).
+definition weight: \forall A,N. T A N \to nat \def 
+   \lambda A,N. 
+   (weight_map A N (\lambda _.O)).
 
-definition tlt : \forall A,N. T A N \to T A N \to Prop \def \lambda A,N. \lambda t1,t2. weight A N t1 < weight A N t2.
+definition tlt: \forall A,N. T A N \to T A N \to Prop \def 
+   \lambda A,N,t1,t2. 
+   weight A N t1 < weight A N t2.