last commit for helena 0.8.1

[helm.git] / helm / software / lambda-delta / src / automath / autCrg.ml

diff --git a/helm/software/lambda-delta/src/automath/autCrg.ml b/helm/software/lambda-delta/src/automath/autCrg.ml
index 388b0c2b9eebbc0bfaeb87c3193b49d9230d8f7d..66de6c3d3c2c8145c2e205a05221afe0bbef5231 100644 (file)
--- a/helm/software/lambda-delta/src/automath/autCrg.ml
+++ b/helm/software/lambda-delta/src/automath/autCrg.ml
@@ -128,7 +128,8 @@ let rec xlate_term f st lenv = function
       let f nw ww = 
          let a = [E.Name (name, true)] in
         let f nt tt = 
-           let b = D.Abst (nt, [ww]) in
+           let nnt = N.infinite (* if N.is_zero nt then N.infinite else nt *) in
+           let b = D.Abst (nnt, [ww]) in
            f nt (D.TBind (a, b, tt))
         in
          let f lenv = xlate_term f st lenv t in