You can clone with
Cannot retrieve contributors at this time
Inductive proof automation for Coqby Sean WilsonThis package contains an inductive proof automation plugin for Coq. This automationincludes a rippling tactic, generalisation heuristics and a counterexample finder tool.This file explains how to compile the code and run the demo file (see theory/demo.v),which includes many examples of theorems that can be automated. See here for documentationabout how the automation works:http://homepages.inf.ed.ac.uk/s0091720/These tactics are still in development. The code and the installation process shouldhopefully be simplified in the future.Note that this code has only been tested under Linux so far.