package coq-waterproof

  1. Overview
  2. Docs
val wp_autorewrite : ?print_hints:bool -> bool -> Backtracking.trace Proofview.tactic -> unit Proofview.tactic

Waterproof autorewrite

This tactic is a rewrite of the coq-core's autorewrite tactic that will only consider current hypothesis as rewrite hints.