[ `Coercion
| `Elim of sort (** elimination principle; if sort is Type, the universe is
* not relevant *)
- | `Record of string list (** inductive type that encodes a record;
- the arguments are the record fields *)
+ | `Record of (string * bool) list (**
+ inductive type that encodes a record; the arguments are
+ the record fields names and if they are coercions *)
| `Projection (** record projection *)
]
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