* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 29/11/2000 *)
-(* *)
-(* This module defines the internal representation of the objects (variables, *)
-(* blocks of (co)inductive definitions and constants) and the terms of cic *)
-(* *)
-(******************************************************************************)
+(*****************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 29/11/2000 *)
+(* *)
+(* This module defines the internal representation of the objects (variables,*)
+(* blocks of (co)inductive definitions and constants) and the terms of cic *)
+(* *)
+(*****************************************************************************)
(* STUFF TO MANAGE IDENTIFIERS *)
type id = string (* the abstract type of the (annotated) node identifiers *)
and sort =
Prop
| Set
- | Type
+ | Type of CicUniv.universe
| CProp
and name =
Name of string
(* depend on new ones. *)
and conjecture = int * context * term
and metasenv = conjecture list
+and substitution = (int * (context * term)) list
+
+
(* a metasenv is a list of declarations of metas in declarations *)
(* order (i.e. [oldest ; ... ; newest]). Older variables can not *)