Module `Proof`Source

Sourcetype t

Sourcetype data = {

sigma : Evd.evar_map;
(*
A representation of the evar_map EJGA wouldn't it better to just return the proofview?
*)
goals : Evar.t list;
(*
Focused goals
*)
entry : Proofview.entry;
(*
Entry for the proofview
*)
stack : (Evar.t list * Evar.t list) list;
(*
A representation of the focus stack
*)
name : Names.Id.t;
(*
The name of the theorem whose proof is being constructed
*)
poly : bool;
(*
polymorphism
*)

}

Sourceval data : t -> data

val start : 
  name:Names.Id.t ->
  poly:bool ->
  ?typing_flags:Declarations.typing_flags ->
  Evd.evar_map ->
  (Environ.env * EConstr.types) list ->
  t

Source

val dependent_start : 
  name:Names.Id.t ->
  poly:bool ->
  ?typing_flags:Declarations.typing_flags ->
  Proofview.telescope ->
  t

Sourceval is_done : t -> bool

Sourceval partial_proof : t -> EConstr.constr list

Sourceval compact : t -> t

Sourceval update_sigma_univs : UGraph.t -> t -> t

update_sigma_univs lifts UState.update_sigma_univs to the proof

Sourcetype 'a focus_kind

Sourceval new_focus_kind : string -> 'a focus_kind

Sourcetype 'a focus_condition

Sourceval no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition

Sourceval done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition

Sourceval focus : 'a focus_condition -> 'a -> int -> t -> t

Sourceval focus_id : 'a focus_condition -> 'a -> Names.Id.t -> t -> t

Sourceexception FullyUnfocused

Sourceexception CannotUnfocusThisWay

Sourceexception NoSuchGoals of int * int

Sourceexception NoSuchGoal of Names.Id.t option

Sourceval unfocus : 'a focus_kind -> t -> unit -> t

Sourceval unfocused : t -> bool

Sourceval unfocus_all : t -> t

Unfocus everything (fail if no allowed).

Sourceexception NoSuchFocus

Sourceval get_at_focus : 'a focus_kind -> t -> 'a

Sourceval is_last_focus : 'a focus_kind -> t -> bool

Sourceval no_focused_goal : t -> bool

Source

val run_tactic : 
  Environ.env ->
  'a Proofview.tactic ->
  t ->
  t * (bool * Proofview_monad.Info.tree) * 'a

Sourceval maximal_unfocus : 'a focus_kind -> t -> t

Sourceval unshelve : t -> t

Sourceval goal_uid : Evar.t -> string

Sourceval pr_proof : t -> Pp.t

Sourceval background_subgoals : t -> Evar.t list

Sourceval all_goals : t -> Evar.Set.t

solve (SelectNth n) tac applies tactic tac to the nth subgoal of the current focused proof. solve SelectAll tac applies tac to all subgoals.

Source

val solve : 
  ?with_end_tac:unit Proofview.tactic ->
  Goal_select.t ->
  int option ->
  unit Proofview.tactic ->
  t ->
  t * bool

Sourceval use_unification_heuristics : unit -> bool

Option telling if unification heuristics should be used.

Source

val refine_by_tactic : 
  name:Names.Id.t ->
  poly:bool ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  unit Proofview.tactic ->
  EConstr.constr * Evd.evar_map

A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may occur. Ideally all code using this function should be rewritten in the monad.

Sourceexception SuggestNoSuchGoals of int * t

Sourceval get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env

Helpers to obtain proof state when in an interactive proof

Sourceval get_proof_context : t -> Evd.evar_map * Environ.env

get_proof_context () gets the goal context for the first subgoal of the proof

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.proofs/Proof/index.html

Module `Proof`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.proofs/Proof/index.html

Module ProofSource

Module `Proof`Source