Module Coq.GoalsSource

Sourcemodule Reified_goal : sig ... end
Sourcetype ('a, 'pp) t = {
  1. goals : 'a list;
  2. stack : ('a list * 'a list) list;
  3. bullet : 'pp option;
  4. shelf : 'a list;
  5. given_up : 'a list;
}
Sourceval equal : ('a -> 'a -> bool) -> ('pp -> 'pp -> bool) -> ('a, 'pp) t -> ('a, 'pp) t -> bool
Sourceval map : f:('a -> 'b) -> g:('pp -> 'pp') -> ('a, 'pp) t -> ('b, 'pp') t
Sourcetype ('goals, 'pp) reified = ('goals Reified_goal.t, 'pp) t
Sourceval reify : ppx:(Environ.env -> Evd.evar_map -> EConstr.t -> 'goals) -> State.Proof.t -> ('goals, Pp.t) reified

Stm-independent goal processor

Sourcemodule Equality : sig ... end