]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brg.ml
improved interface for brgEnvironment
[helm.git] / helm / software / lambda-delta / basic_rg / brg.ml
index eaaeb6e6054c8c3fc426b74cd776f0256e89985d..45777ead4f41d41dcc1ab793d5473a35b54df016 100644 (file)
@@ -21,6 +21,6 @@ type term = Sort of int                     (* hierarchy index *)
          | Appl of term * term             (* argument, function *)
          | Bind of id * bind * term * term (* name, binder, content, scope *)
 
-type obj = bind * term (* binder, contents *)
+type obj = int * uri * bind * term (* age, uri, binder, contents *)
 
-type item = (obj * uri) option (* uri, object *)
+type item = obj option