aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/changes.txt
AgeCommit message (Expand)Author
2016-12-02Merge remote-tracking branch 'github/pr/372' into v8.6Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/368' into v8.6Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/369' into v8.6Maxime Dénès
2016-11-21(v8.6) Update dev/doc/changes.txt with HintsResolveEntry changesJason Gross
2016-11-21(v8.6) Update dev/doc/changes with things about mem_named_contextJason Gross
2016-11-21(v8.6) Make a note about wit_constr and Constrarg in dev/doc/changesJason Gross
2016-11-21(v8.6) Add example in dev/doc/changes involving Tacmach.projectJason Gross
2016-11-16[doc] Mention XML protocol on changes.Emilio Jesus Gallego Arias
2016-10-20[search] Don't build intermediate lists in search.Emilio Jesus Gallego Arias
2016-10-17More on making the lexer more functional (continuing b8ae2de5 andHugo Herbelin
2016-08-16Merge PR #237 into v8.6Pierre-Marie Pédrot
2016-07-05FIX: "dev/doc/changes.txt"Matej Kosik
2016-07-04Add a renaming of Tacexpr.TacDynamicJason Gross
2016-07-03Mention recent renaming of files in dev/doc/changes.txt.Maxime Dénès
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-25[doc] Update changes for feedback.Emilio Jesus Gallego Arias
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-06-09Documenting API changes in dev/doc/changes.txt.Pierre-Marie Pédrot
2016-06-08Add an explicit replacement rule for Refine moduleJason Gross
2016-06-02A slight phase of documentation and uniformization of names ofHugo Herbelin
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-03-20Documenting changes.Pierre-Marie Pédrot
2016-03-18Documenting the change of EXTEND macros.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
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-05-08Isolating a function "make_abstraction", new name of "letin_abstract",Hugo Herbelin
2014-05-08Renaming new_induct -> induction; new_destruct -> destruct.Hugo Herbelin
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2012-05-29Some documentation of recent changes concerning interfacesletouzey
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-02-11Update changelogsglondu
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-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
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-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin