type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]
type lc_kind = Irl of int | Ctx of term list
and local_context = int * lc_kind (* shift (0 -> no shift),
type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]
type lc_kind = Irl of int | Ctx of term list
and local_context = int * lc_kind (* shift (0 -> no shift),