package coq

  1. Overview
  2. Docs

Module Compacted.DeclarationSource

Sourcetype ('constr, 'types) pt =
  1. | LocalAssum of Names.Id.t binder_annot list * 'types
  2. | LocalDef of Names.Id.t binder_annot list * 'constr * 'types
Sourceval map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
Sourceval of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt
Sourceval to_named_context : ('c, 't) pt -> ('c, 't) Named.pt