aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/changes.txt
Commit message (Expand)AuthorAge
* CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\
| * More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
* | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
* | Documenting API changes.Gravatar Pierre-Marie Pédrot2016-09-15
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: removing "Termops.compact_named_context_reverse" functionGravatar Matej Kosik2016-08-26
* | | CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"Gravatar Matej Kosik2016-08-26
* | | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
* | | CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
* | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
| |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Merge PR #237 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
* | FIX: "dev/doc/changes.txt"Gravatar Matej Kosik2016-07-05
| * Add a renaming of Tacexpr.TacDynamicGravatar Jason Gross2016-07-04
|/
* Mention recent renaming of files in dev/doc/changes.txt.Gravatar Maxime Dénès2016-07-03
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* [doc] Update changes for feedback.Gravatar Emilio Jesus Gallego Arias2016-06-25
* [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
* Documenting API changes in dev/doc/changes.txt.Gravatar Pierre-Marie Pédrot2016-06-09
* Add an explicit replacement rule for Refine moduleGravatar Jason Gross2016-06-08
* A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Documenting changes.Gravatar Pierre-Marie Pédrot2016-03-20
* Documenting the change of EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-18
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* 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
* 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
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Some documentation of recent changes concerning interfacesGravatar letouzey2012-05-29
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Update changelogsGravatar glondu2011-02-11
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 09:13:37 +0000