X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2Fbrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2Fbrg.ml;h=bc6eb57277787753485621798a8b3949597f7e92;hb=22fd9c98a22929f0319286c0693fcdaee43a72df;hp=d2a0b99873cd93fd146801a7e17fb53bbb1355c7;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/helm/software/lambda-delta/src/basic_rg/brg.ml b/helm/software/lambda-delta/src/basic_rg/brg.ml
index d2a0b9987..bc6eb5727 100644
--- a/helm/software/lambda-delta/src/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/src/basic_rg/brg.ml
@@ -13,14 +13,15 @@
 (* note          : ufficial basic lambda-delta *) 
 
 module E = Entity
+module N = Level
 
 type uri = E.uri
 type id = E.id
 type attrs = E.attrs
 
-type bind = Void         (*      *)
-          | Abst of term (* type *)
-          | Abbr of term (* body *)
+type bind = Void                   (*             *)
+          | Abst of N.level * term (* level, type *)
+          | Abbr of term           (* body        *)
 
 and term = Sort of attrs * int         (* attrs, hierarchy index *)
          | LRef of attrs * int         (* attrs, position index *)
@@ -43,7 +44,7 @@ let mk_uri si root s =
 
 (* Currified constructors ***************************************************)
 
-let abst w = Abst w
+let abst n w = Abst (n, w)
 
 let abbr v = Abbr v
 
@@ -55,7 +56,7 @@ let appl a u t = Appl (a, u, t)
 
 let bind a b t = Bind (a, b, t)
 
-let bind_abst a u t = Bind (a, Abst u, t)
+let bind_abst n a u t = Bind (a, Abst (n, u), t)
 
 let bind_abbr a v t = Bind (a, Abbr v, t)