Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package coq-waterproof
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val is_blank : Evd.evar_map -> Evar.t -> boolChecks whether a given evar is a blank (entered by the user with the `_` syntax) in the evar_map.
val refine_goal_with_evar : string -> unit Proofview.tacticRefines the current goal with just a new named evar, the name of which is based on the input string. The use of this is to replace unnamed evars with named ones, so that the user can refer to them later.
val blank_evars_in_term : Evd.econstr -> Evar.t list Proofview.tacticA tactic that resturns a list of all evars in a term (= Evd.econstr) that were introduced by the user as a blank and have not been resolved yet.