\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module N = Level
+module N = Layer
type ix = int (* index *)
| Th (* theorem *)
type bind =
-(* name, real?, domain *)
- | Abst of (id * bool * term) list
+(* layer, name, real?, domain *)
+ | Abst of N.layer * id * bool * term
(* name, bodies *)
- | Abbr of (id * term) list
-(* names *)
- | Void of id list
+ | Abbr of id * term
+(* name *)
+ | Void of id
+
+and lenv = bind list
and term =
(* level *)
(* named level *)
| NSrt of id
(* index, offset *)
- | LRef of ix * ix
+ | LRef of ix
(* name *)
| NRef of id
(* domain, element *)
| Cast of term * term
(* arguments, function *)
- | Appl of term list * term
-(* level, binder, scope *)
- | Bind of N.level * bind * term
+ | Appl of term * term
+(* environment, scope *)
+ | Proj of lenv * term
(* function, arguments *)
| Inst of term * term list
-(* level, strong?, label, source, target *)
- | Impl of N.level * bool * id * term * term
type command =
(* required files: names *)
(* section: Some id = open, None = close last *)
| Section of id option
(* entity: main?, class, name, info, contents *)
- | Entity of bool * kind * N.level * id * info * term
+ | Constant of bool * kind * id * info * term
(* predefined generated entity: arguments *)
| Generate of term list