package coq-waterproof

You can search for identifiers within the package.

in-package search v0.2.0

coq-waterproof.plugin
- Waterproof
  - Backtracking
  - Databases
  - Exceptions
  - G_waterproof
  - Hint_dataset
  - Hint_dataset_declarations
  - Proofutils
    
    Mergeable
    
    StringMap
    
    TraceTactics
    
    TypedTactics
    
    M
  - Waterprove
  - Wp_auto
  - Wp_eauto
  - Wp_evars
  - Wp_ffi
  - Wp_rewrite

Legend:
Library
Module
Module type
Parameter
Class
Class type

val esearch : 
  bool ->
  int ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db list ->
  Pp.t list ->
  Pp.t list ->
  Backtracking.trace Proofview.tactic

Searches a sequence of at most n tactics within db_list and lems that solves the goal

The goal can contain evars

val wp_eauto : 
  bool ->
  int ->
  Tactypes.delayed_open_constr list ->
  string list ->
  Backtracking.trace Proofview.tactic

Waterproof eauto

This function is a rewrite around Eauto.eauto with the same arguments to be able to retrieve which hints have been used in case of success.

The code structure has been rearranged to match the one of wp_auto.wp_auto.

val rwp_eauto : 
  bool ->
  int ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db_name list ->
  Pp.t list ->
  Pp.t list ->
  Backtracking.trace Proofview.tactic

Restricted Waterproof eauto

This function acts the same as wp_auto but will fail if all proof found contain at least one must-use lemma that is unused or one hint that is in the forbidden list.