Up – Package index » coq-serapi » Library coq-serapi.serlib_extra » Serlib_extra » Ser_stm

Module `Serlib_extra.Ser_stm`Source

coq-serapi
- CHANGES
- README
- Library coq-serapi.coq
  - Coq
- Library coq-serapi.serapi_v8_14
  - Serapi
- Library coq-serapi.serlib
  - Serlib
- Library coq-serapi.serlib_extra
  - Serlib_extra
- Library coq-serapi.sertop_v8_12
  - Sertop
- Library serlib_btauto
  - Serlib_btauto
- Library serlib_cc
  - Serlib_cc
- Library serlib_extraction
  - Serlib_extraction
- Library serlib_firstorder
  - Serlib_firstorder
- Library serlib_funind
  - Serlib_funind
- Library serlib_ltac
  - Serlib_ltac
- Library serlib_ltac2
  - Serlib_ltac2
- Library serlib_micromega
  - Serlib_micromega
- Library serlib_micromega_core
  - Serlib_micromega_core
- Library serlib_number_string_notation_plugin
  - Serlib_number_string_notation_plugin
- Library serlib_ring
  - Serlib_ring
- Library serlib_ssr
  - Serlib_ssr
- Library serlib_ssrmatching
  - Serlib_ssrmatching
- Library serlib_tauto
  - Serlib_tauto
- Library serlib_zify
  - Serlib_zify
- Sources

Sourcetype focus = Stm.focus

Sourceval sexp_of_focus : focus -> Sexplib0.Sexp.t

Sourceval focus_of_sexp : Sexplib0.Sexp.t -> focus

Sourcetype add_focus = Stm.add_focus

Sourceval sexp_of_add_focus : add_focus -> Sexplib0.Sexp.t

Sourceval add_focus_of_sexp : Sexplib0.Sexp.t -> add_focus