package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Trace : sig ... end
type lazy_msg = Environ.env -> Evd.evar_map -> Pp.t
module Info : sig ... end
type goal = Evar.t
type goal_with_state
val drop_state : goal_with_state -> goal
val get_state : goal_with_state -> StateStore.t
val goal_with_state : goal -> StateStore.t -> goal_with_state
val with_empty_state : goal -> goal_with_state
val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
type proofview = {
  1. solution : Evd.evar_map;
  2. comb : goal_with_state list;
}
module P : sig ... end
module Logical : sig ... end
module type State = sig ... end
module type Reader = sig ... end
module type Writer = sig ... end
module Pv : sig ... end
module Solution : sig ... end
module Comb : sig ... end
module Env : sig ... end
module Status : sig ... end
module InfoL : sig ... end