package coq-serapi
-
coq-serapi.serapi_v8_14
-
coq-serapi.serlib
-
-
coq-serapi.serlib.extraction_plugin
-
coq-serapi.serlib.firstorder_plugin
-
coq-serapi.serlib.funind_plugin
-
coq-serapi.serlib.ltac
-
coq-serapi.serlib.ring_plugin
-
coq-serapi.serlib.ssreflect_plugin
-
coq-serapi.serlib.ssrmatching_plugin
-
coq-serapi.sertop_v8_12
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type ser_opts = {
in_chan : in_channel;
out_chan : out_channel;
(*Input/Output channels
*)printer : Sertop_ser.ser_printer;
(*Printer type
*)debug : bool;
(*Enable Coq debug mode
*)allow_sprop : bool;
(*Allow using the proof irrelevant SProp sort
*)indices_matter : bool;
(*Indices of indexes contribute to inductive level
*)print0 : bool;
(*End every answer with
*)\0
lheader : bool;
(*Print lenght header (deprecated)
*)no_init : bool;
(*Whether to create the initial document
*)no_prelude : bool;
(*Whether to load stdlib's prelude
*)topfile : string option;
(*Top name is derived from topfile name
*)ml_path : string list;
vo_path : Loadpath.vo_path list;
(*From -R and -Q options usually
*)async : Sertop_init.async_flags;
(*Async flags
*)
}
Options for the sertop interactive toplevel
val ser_loop : ser_opts -> unit
ser_loop opts
main se(xp)r-protocol interactive loop
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>