]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brg.ml
basic_rg: improved interface, unwind removed from applicability check
[helm.git] / helm / software / lambda-delta / basic_rg / brg.ml
index e42db3319b5739aea2bb9f00218b102f411adf35..8b0d5453391683ee65e64d7d299f9b882334c4eb 100644 (file)
@@ -12,8 +12,8 @@
 (* kernel version: basic, relative, global *)
 (* note          : ufficial basic lambda-delta *) 
 
-type uri = NUri.uri
-type id = Aut.id
+type uri = Common.uri
+type id = Common.id
 
 type bind = Void         (* exclusion *)
           | Abst of term (* abstraction *)
@@ -31,9 +31,9 @@ and attr = Name of bool * id   (* real?, name *)
 
 and attrs = attr list
 
-type obj = int * uri * bind (* age, uri, binder, contents *)
+type obj = bind Common.obj (* age, uri, binder *)
 
-type item = obj option
+type item = bind Common.item
 
 type context = (attrs * bind) list (* attrs, binder *)