]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/complete_rg/crg.ml
- we are moving from old (patched) management of sort inclusion
[helm.git] / helm / software / helena / src / complete_rg / crg.ml
index 87fbaf3e252177fa5cbf039ca1290c545ffcf2eb..673b3a0baf523434b8d52c74d51cf807f8e4a2f8 100644 (file)
 (* note          : fragment of complete \lambda\delta serving as abstract layer *) 
 
 module C = Cps
-module N = Level
+module N = Layer
 module E = Entity
 
 type uri = E.uri
 type id = E.id
 type attrs = E.node_attrs
 
-type bind = Abst of N.level * term      (* level, type *)
+type bind = Abst of N.layer * term      (* layer, type *)
           | Abbr of term                (* body *)
           | Void                        (* *)