type extra_goals = extra_goal listtype extra_goals_postprocessing =
extra_goals ->
State.t ->
State.t * extra_goalsval extra_goals_postprocessing : extra_goals_postprocessing State.componentval pp_ty_ast :
Ppx_deriving_runtime.Format.formatter ->
ty_ast ->
Ppx_deriving_runtime.unittype 'a embedding = depth:int -> State.t -> 'a -> State.t * term * extra_goalstype 'a readback = depth:int -> State.t -> term -> State.t * 'a * extra_goalsval pp :
'a. (Ppx_deriving_runtime.Format.formatter ->
'a ->
Ppx_deriving_runtime.unit) ->
Ppx_deriving_runtime.Format.formatter ->
'a t ->
Ppx_deriving_runtime.unitval show :
'a. (Ppx_deriving_runtime.Format.formatter ->
'a ->
Ppx_deriving_runtime.unit) ->
'a t ->
Ppx_deriving_runtime.stringval need_par : prec_level option -> prec_level -> boolval with_par : prec_level option -> prec_level -> string -> stringval show_ty_ast : ?prec:prec_level -> ty_ast -> stringval term_of_extra_goal : extra_goal -> term