- initial support for abstractions with explicit levels

[helm.git] / helm / software / lambda-delta / src / text / txtTxt.ml

diff --git a/helm/software/lambda-delta/src/text/txtTxt.ml b/helm/software/lambda-delta/src/text/txtTxt.ml
index 1d501fe0d7221faa4157f2268da48ae641ea732c..d2c85cb921a9ac4d3e492b0e1b70dd03d0367fbc 100644 (file)
--- a/helm/software/lambda-delta/src/text/txtTxt.ml
+++ b/helm/software/lambda-delta/src/text/txtTxt.ml
@@ -18,16 +18,16 @@ let rec contract f = function
    | T.Inst (t, vs)           ->
       let tt = T.Appl (List.rev vs, t) in 
       contract f tt
-   | T.Impl (false, id, w, t) ->
-      let tt = T.Bind (T.Abst [id, false, w], t) in 
+   | T.Impl (n, false, id, w, t) ->
+      let tt = T.Bind (n, T.Abst [id, false, w], t) in 
       contract f tt      
-   | T.Impl (true, id, w, t)  -> 
+   | T.Impl (n, true, id, w, t)  -> 
       let f = function
-         | T.Bind (T.Abst [xw], T.Bind (T.Abst xws, tt)) ->
-            f (T.Bind (T.Abst (xw :: xws), tt))
+         | T.Bind (n, T.Abst [xw], T.Bind (_, T.Abst xws, tt)) ->
+            f (T.Bind (n, T.Abst (xw :: xws), tt))
         | tt                                            -> f tt
       in
-      let tt = T.Impl (false, id, w, t) in
+      let tt = T.Impl (n, false, id, w, t) in
       contract f tt
    | T.Sort _ 
    | T.NSrt _     
@@ -41,8 +41,8 @@ let rec contract f = function
       let f tt vvs = f (T.Appl (vvs, tt)) in
       let f tt = C.list_map (f tt) contract vs in
       contract f t      
-   | T.Bind (b, t)            ->
-      let f tt bb = f (T.Bind (bb, tt)) in
+   | T.Bind (n, b, t)            ->
+      let f tt bb = f (T.Bind (n, bb, tt)) in
       let f tt = contract_binder (f tt) b in
       contract f t