(********************************* TERMS ************************************)
type universe = (bool * NUri.uri) list
- (* Max of non-empty list of named universes, or their successor (when true) *)
+ (* Max of non-empty list of named universes, or their successor (when true)
+ * The empty list represents type0 *)
type sort = Prop | Type of universe
-type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]
+type implicit_annotation = [ `Closed | `Type | `Hole | `Term | `Typeof of int ]
type lc_kind = Irl of int | Ctx of term list