X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2Fbrg.ml;h=e3c5866818c2d8e1a8db71a42d3d100ecd84d057;hb=8049c166a37789d7a1b1ca1c3a1174712bbf87ba;hp=52ec4728f0a6ffe13536cb940adfc55cf02bee37;hpb=8a4c83c6341976f2bb70eb44a0c70f2aa95ad3ea;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml index 52ec4728f..e3c586681 100644 --- a/helm/software/lambda-delta/basic_rg/brg.ml +++ b/helm/software/lambda-delta/basic_rg/brg.ml @@ -12,8 +12,8 @@ (* kernel version: basic, relative, global *) (* note : ufficial basic lambda-delta *) -type uri = Item.uri -type id = Item.id +type uri = Entity.uri +type id = Entity.id type attr = Name of bool * id (* real?, name *) | Apix of int (* additional position index *) @@ -31,9 +31,9 @@ and term = Sort of attrs * int (* attrs, hierarchy index *) | Appl of attrs * term * term (* attrs, argument, function *) | Bind of bind * term (* binder, scope *) -type obj = bind Item.obj (* age, uri, binder *) +type entry = bind Entity.entry (* age, uri, binder *) -type item = bind Item.item +type entity = bind Entity.entity type lenv = Null (* Cons: tail, relative local environment, binder *)