aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqschemes.ml
Commit message (Expand)AuthorAge
* Eqschemes: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
* Changed name of internally defined "_sym" scheme to avoid confusion with Logi...Gravatar herbelin2011-07-16
* Remove "init" label from Termops.it_mk* specialized functionsGravatar glondu2010-09-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New pass on inductive schemesGravatar herbelin2010-05-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Compatibility ocaml <= 3.09Gravatar herbelin2009-11-10
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Quick fix for restoring a left-to-right rewriting lemma compatibleGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08