package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

This files implements auto and related automation tactics

val compute_secvars : Proofview.Goal.t -> Names.Id.Pred.t
val default_search_depth : int Stdlib.ref
val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
val unify_resolve : Unification.unify_flags -> Hints.hint -> unit Proofview.tactic

Try unification with the precompiled clause, then use registered Apply

ConclPattern concl pat tacast: if the term concl matches the pattern pat, (in sense of Pattern.somatches, then replace ?1 ?2 metavars in tacast by the right values to build a tactic

The Auto tactic

The use of the "core" database can be de-activated by passing "nocore" amongst the databases.

val auto : ?debug:Hints.debug -> int -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list -> unit Proofview.tactic

Auto with more delta.

val default_auto : unit Proofview.tactic

auto with default search depth and with the hint database "core"

val full_auto : ?debug:Hints.debug -> int -> Tactypes.delayed_open_constr list -> unit Proofview.tactic

auto with all hint databases

val default_full_auto : unit Proofview.tactic

auto with default search depth and with all hint databases

val gen_auto : ?debug:Hints.debug -> int option -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic

The generic form of auto (second arg None means all bases)

val h_auto : ?debug:Hints.debug -> int option -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic

The hidden version of auto

Trivial

val gen_trivial : ?debug:Hints.debug -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
val full_trivial : ?debug:Hints.debug -> Tactypes.delayed_open_constr list -> unit Proofview.tactic
val h_trivial : ?debug:Hints.debug -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list option -> unit Proofview.tactic
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct