]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brg.ml
- we are moving from old (patched) management of sort inclusion
[helm.git] / helm / software / helena / src / basic_rg / brg.ml
index cdfa93c6ef1e15d539ef928cfbc0f48e0d8b2917..9cf2f47d2069e14dcf66f77d15a458dd388bdfee 100644 (file)
 (* kernel version: basic, relative, global *)
 (* note          : ufficial basic \lambda\delta *) 
 
-module N = Level
+module N = Layer
 module E = Entity
 
 type uri = E.uri
 type attrs = E.node_attrs
 
 type bind = Void                   (*             *)
-          | Abst of N.level * term (* level, type *)
+          | Abst of N.layer * term (* layer, type *)
           | Abbr of term           (* body        *)
 
 and term = Sort of attrs * int         (* attrs, hierarchy index *)