Up – Package index » coq-lsp » Library coq-lsp.fleche » Fleche » Info » Goals

Module `Info.Goals`Source

We move towards a more modular design here, for preprocessing

coq-lsp
- CHANGES
- README
- Library Astdump_plugin
  - Astdump_plugin
- Library Example_plugin
  - Example_plugin
- Library Goaldumpl_plugin
  - Goaldumpl_plugin
- Library Savevo_plugin
  - Savevo_plugin
- Library coq-lsp.coq
  - Coq
- Library coq-lsp.fleche
  - Fleche
- Library coq-lsp.lang
  - Lang
- Library coq-lsp.lsp
  - Lsp
- Library coq-lsp.petanque
  - Petanque
- Library coq-lsp.plugin
- Library fleche_waterproof
  - Fleche_waterproof
- Library petanque_json
  - Petanque_json
- Sources

val goals : 
  token:Coq.Limits.Token.t ->
  st:Coq.State.t ->
  (Pp.t Coq.Goals.reified_pp option, Loc.t) Coq.Protect.E.t

Sourceval program : st:Coq.State.t -> Declare.OblState.View.t Names.Id.Map.t