aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
Commit message (Expand)AuthorAge
...
* Univs: More info for developers.Gravatar Matthieu Sozeau2015-10-02
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Change Ltac constr matching semantics to consider universes when merging twoGravatar Matthieu Sozeau2014-06-15
* A little bit of documentation about V5.10 and V6.3 and V7.Gravatar Hugo Herbelin2014-06-01
* Isolating a function "make_abstraction", new name of "letin_abstract",Gravatar Hugo Herbelin2014-05-08
* Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
* Add incompatibilities paragraph in doc about universe polymorphism.Gravatar Matthieu Sozeau2014-05-06
* Add doc on the new API for universe polymorphism and primitive projectionsGravatar Matthieu Sozeau2014-05-06
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
* Makefile: re-introduce 2 phases to avoid make strange -include'sGravatar Pierre Letouzey2014-02-27
* A file listing old svn branches and tagsGravatar letouzey2013-11-18
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Revert "remove -rectypes except for term.ml"Gravatar mdenes2013-01-22
* remove -rectypes except for term.mlGravatar letouzey2012-10-06
* Remove broken makefile option NO_RECOMPILE_LIBGravatar letouzey2012-09-20
* Some documentation of recent changes concerning interfacesGravatar letouzey2012-05-29
* debugging.txt: no more typing of #use "include" if using .ocamlinitGravatar letouzey2011-10-15
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Moving never-used comments from Zhints.v to dev/doc so as not toGravatar herbelin2011-10-01
* A few comments and a dev file to summarize issues with unificationGravatar herbelin2011-06-13
* Update changelogsGravatar glondu2011-02-11
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
* Fixed a bug in pretty-printing "induction" and "destruct" due to aGravatar herbelin2010-06-13
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
* Updated performance analysis fileGravatar herbelin2010-06-06
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Removing redundant internal variants of apply tactic and simplification of ML...Gravatar herbelin2010-04-14
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...Gravatar letouzey2010-03-04
* Few misc. updates.Gravatar herbelin2010-01-04
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed clash names in Relations (see bug report #2152) and make namesGravatar herbelin2009-10-08
* Mise à jour du document de révision de la stdlib et déplacement de laGravatar herbelin2009-08-14
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Moved and completed the history of Coq versions from theGravatar herbelin2009-05-24
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Correction du patch -rectypes pour ocaml 3.10Gravatar vsiles2009-04-14
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 07:59:33 +0000