type sort = Prop | Type of universe
-type implicit_annotation = [ `Closed | `Type | `Hole | `Term | `Typeof of int ]
+type implicit_annotation =
+ [ `Closed | `Type | `Hole | `Term | `Typeof of int | `Vector ]
type lc_kind = Irl of int | Ctx of term list