]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brg.ml
log facility, initial environment for basic_rg
[helm.git] / helm / software / lambda-delta / basic_rg / brg.ml
index 09d2f247a33f8078193cee8b688f2a1489df1b69..eaaeb6e6054c8c3fc426b74cd776f0256e89985d 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 entry = uri * bind * term (* uri, binder, contents *)
+type obj = bind * term (* binder, contents *)
 
-type item = entry option
+type item = (obj * uri) option (* uri, object *)