Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val hyp_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a hyp -> Yojson.Safe.t
val hyp_of_yojson :
'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a hyp Ppx_deriving_yojson_runtime.error_or
val info_to_yojson : info -> Yojson.Safe.t
val info_of_yojson : Yojson.Safe.t -> info Ppx_deriving_yojson_runtime.error_or
val reified_goal_to_yojson :
'a. ('a -> Yojson.Safe.t) ->
'a reified_goal ->
Yojson.Safe.t
val reified_goal_of_yojson :
'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a reified_goal Ppx_deriving_yojson_runtime.error_or
type 'a goals = 'a Coq.Goals.goals = {
goals : 'a list;
stack : ('a list * 'a list) list;
bullet : Pp.t option;
shelf : 'a list;
given_up : 'a list;
}
val goals_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a goals -> Yojson.Safe.t
val goals_of_yojson :
'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a goals Ppx_deriving_yojson_runtime.error_or
type reified_pp = Pp.t reified_goal goals
val reified_pp_to_yojson : reified_pp -> Yojson.Safe.t
val reified_pp_of_yojson :
Yojson.Safe.t ->
reified_pp Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> reified_pp Ppx_deriving_yojson_runtime.error_or