package coq

You can search for identifiers within the package.

in-package search v0.2.0

Module `Eauto`Source

Sourceval e_assumption : unit Proofview.tactic

Sourceval registered_e_assumption : unit Proofview.tactic

val e_give_exact : 
  ?flags:Unification.unify_flags ->
  EConstr.constr ->
  unit Proofview.tactic

Source

val gen_eauto : 
  ?debug:Hints.debug ->
  (bool * int) ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db_name list option ->
  unit Proofview.tactic

Source

val eauto_with_bases : 
  ?debug:Hints.debug ->
  (bool * int) ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db list ->
  unit Proofview.tactic

Source

val autounfold : 
  Hints.hint_db_name list ->
  Locus.clause ->
  unit Proofview.tactic

Source

val autounfold_tac : 
  Hints.hint_db_name list option ->
  Locus.clause ->
  unit Proofview.tactic

Source

val autounfold_one : 
  Hints.hint_db_name list ->
  Locus.hyp_location option ->
  unit Proofview.tactic

Sourceval make_depth : int option -> int

Sourceval make_dimension : int option -> int option -> bool * int

package coq

Module EautoSource

Module `Eauto`Source