aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqschemes.ml
Commit message (Expand)AuthorAge
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (tactics)Gravatar ppedrot2012-11-25
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* 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