(* *)
(*****************************************************************************)
+(* $Id$ *)
+
(* STUFF TO MANAGE IDENTIFIERS *)
type id = string (* the abstract type of the (annotated) node identifiers *)
type 'term explicit_named_substitution = (UriManager.uri * 'term) list
and anncontext = annhypothesis list
;;
+type lazy_term =
+ context -> metasenv -> CicUniv.universe_graph ->
+ term * metasenv * CicUniv.universe_graph
+
type anntarget =
Object of annobj (* if annobj is a Constant, this is its type *)
| ConstantBody of annobj