aboutsummaryrefslogtreecommitdiff
path: root/tactics/eqschemes.ml
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-08-08State Transaction Machinegareuselesinge
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-07-29Eqschemes: generic equality on constr replaced by eq_constrpuech
2011-07-16Changed name of internally defined "_sym" scheme to avoid confusion with Logi...herbelin
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-29New pass on inductive schemesherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-10Compatibility ocaml <= 3.09herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-09Quick fix for restoring a left-to-right rewriting lemma compatibleherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:38:30 +0000