package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Trace : sig ... end
type lazy_msg = unit -> 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;
  3. shelf : goal list;
}
module P : sig ... end
module Logical : sig ... end
module type State = 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 Shelf : sig ... end
module Giveup : sig ... end
module InfoL : sig ... end