(********************************* 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 | `Vector ]
type lc_kind = Irl of int | Ctx of term list