package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.18.0.0.18.1.tbz
sha256=3958ec27603e3f927a74f11d02d98390e8ecda942bb23f37ff6fa575b31a8158
sha512=d33f9340de6e1426a42192da3610a7636b0201baa166cf788926b866738ae299219439bc22112cc81591c565dd857f66e53a41a3cfe420844f31fb6077abe57b
doc/serlib_ltac/Serlib_ltac/Ser_tacentries/index.html
Module Serlib_ltac.Ser_tacentries
Source
Source
type 'a grammar_tactic_prod_item_expr =
'a Ltac_plugin.Tacentries.grammar_tactic_prod_item_expr
Source
val sexp_of_grammar_tactic_prod_item_expr :
('a -> Sexplib0.Sexp.t) ->
'a grammar_tactic_prod_item_expr ->
Sexplib0.Sexp.t
Source
val grammar_tactic_prod_item_expr_of_sexp :
(Sexplib0.Sexp.t -> 'a) ->
Sexplib0.Sexp.t ->
'a grammar_tactic_prod_item_expr
Source
val hash_fold_grammar_tactic_prod_item_expr :
(Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) ->
Ppx_hash_lib.Std.Hash.state ->
'a grammar_tactic_prod_item_expr ->
Ppx_hash_lib.Std.Hash.state
Source
val compare_grammar_tactic_prod_item_expr :
('a -> 'a -> int) ->
'a grammar_tactic_prod_item_expr ->
'a grammar_tactic_prod_item_expr ->
int
Source
val hash_fold_raw_argument :
Ppx_hash_lib.Std.Hash.state ->
raw_argument ->
Ppx_hash_lib.Std.Hash.state
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>