(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

type ix = int (* index *)

type id = string (* identifier *)

type comm = string (* comment *)

type bind = Abst of (id * term) list (* name, domain *)
          | Abbr of (id * term) list (* name, bodies *)
          | Void of id list          (* names        *)

and term = Sort of ix               (* level               *)
         | NSrt of id               (* named level         *)
	 | LRef of ix * ix          (* index, offset       *)
	 | NRef of id               (* name                *)
	 | Cast of term * term      (* domain, element     *)
	 | Appl of term list * term (* arguments, function *)
	 | Bind of bind * term      (* binder, scope       *)

type entity = Section of id option              (* section: Some id = open, None = close last *)
	    | Global of bool * id * comm * term (* global entity: false = decl, true = def    *)