aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
AgeCommit message (Expand)Author
2015-10-02Updating versions history with data from Gérard.Hugo Herbelin
2015-10-02Update the history of versions with recent versions.Hugo Herbelin
2015-10-02Univs: More info for developers.Matthieu Sozeau
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-08-18A reorganization of the "assert" tactics (hopefully uniform namingHugo Herbelin
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-28Moved code for finding subterms (pattern, induction, set, generalize, ...)Hugo Herbelin
2014-06-15Change Ltac constr matching semantics to consider universes when merging twoMatthieu Sozeau
2014-06-01A little bit of documentation about V5.10 and V6.3 and V7.Hugo Herbelin
2014-05-08Isolating a function "make_abstraction", new name of "letin_abstract",Hugo Herbelin
2014-05-08Renaming new_induct -> induction; new_destruct -> destruct.Hugo Herbelin
2014-05-06Add incompatibilities paragraph in doc about universe polymorphism.Matthieu Sozeau
2014-05-06Add doc on the new API for universe polymorphism and primitive projectionsMatthieu Sozeau
2014-03-02Set officially the minimal OCaml requirement to 3.12.1Pierre Letouzey
2014-02-27Makefile: re-introduce 2 phases to avoid make strange -include'sPierre Letouzey
2013-11-18A file listing old svn branches and tagsletouzey
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-01-22Revert "remove -rectypes except for term.ml"mdenes
2012-10-06remove -rectypes except for term.mlletouzey
2012-09-20Remove broken makefile option NO_RECOMPILE_LIBletouzey
2012-05-29Some documentation of recent changes concerning interfacesletouzey
2011-10-15debugging.txt: no more typing of #use "include" if using .ocamlinitletouzey
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-01Moving never-used comments from Zhints.v to dev/doc so as not toherbelin
2011-06-13A few comments and a dev file to summarize issues with unificationherbelin
2011-02-11Update changelogsglondu
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
2010-06-13Fixed a bug in pretty-printing "induction" and "destruct" due to aherbelin
2010-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
2010-06-06Updated performance analysis fileherbelin
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-04-14Removing redundant internal variants of apply tactic and simplification of ML...herbelin
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2010-03-04Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...letouzey
2010-01-04Few misc. updates.herbelin
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-08Fixed clash names in Relations (see bug report #2152) and make namesherbelin
2009-08-14Mise à jour du document de révision de la stdlib et déplacement de laherbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-05-24Moved and completed the history of Coq versions from theherbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:53:54 +0000