index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
dev
/
doc
/
changes.txt
Age
Commit message (
Expand
)
Author
2016-12-02
Merge remote-tracking branch 'github/pr/372' into v8.6
Maxime Dénès
2016-12-02
Merge remote-tracking branch 'github/pr/368' into v8.6
Maxime Dénès
2016-12-02
Merge remote-tracking branch 'github/pr/369' into v8.6
Maxime Dénès
2016-11-21
(v8.6) Update dev/doc/changes.txt with HintsResolveEntry changes
Jason Gross
2016-11-21
(v8.6) Update dev/doc/changes with things about mem_named_context
Jason Gross
2016-11-21
(v8.6) Make a note about wit_constr and Constrarg in dev/doc/changes
Jason Gross
2016-11-21
(v8.6) Add example in dev/doc/changes involving Tacmach.project
Jason 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-17
More on making the lexer more functional (continuing b8ae2de5 and
Hugo Herbelin
2016-08-16
Merge PR #237 into v8.6
Pierre-Marie Pédrot
2016-07-05
FIX: "dev/doc/changes.txt"
Matej Kosik
2016-07-04
Add a renaming of Tacexpr.TacDynamic
Jason Gross
2016-07-03
Mention recent renaming of files in dev/doc/changes.txt.
Maxime Dénès
2016-07-01
Add and document match, fix and cofix reduction flags.
Maxime Dénès
2016-07-01
Separate 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-09
Documenting API changes in dev/doc/changes.txt.
Pierre-Marie Pédrot
2016-06-08
Add an explicit replacement rule for Refine module
Jason Gross
2016-06-02
A slight phase of documentation and uniformization of names of
Hugo Herbelin
2016-05-31
Feedback cleanup
Emilio Jesus Gallego Arias
2016-03-20
Documenting changes.
Pierre-Marie Pédrot
2016-03-18
Documenting the change of EXTEND macros.
Pierre-Marie Pédrot
2016-02-09
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2014-12-09
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-09-12
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-08-18
A reorganization of the "assert" tactics (hopefully uniform naming
Hugo Herbelin
2014-08-18
Reorganisation of intropattern code
Hugo Herbelin
2014-08-01
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-06-28
Moved code for finding subterms (pattern, induction, set, generalize, ...)
Hugo Herbelin
2014-05-08
Isolating a function "make_abstraction", new name of "letin_abstract",
Hugo Herbelin
2014-05-08
Renaming new_induct -> induction; new_destruct -> destruct.
Hugo Herbelin
2013-05-09
A uniformization step around understand_* and interp_* functions.
herbelin
2012-05-29
Some documentation of recent changes concerning interfaces
letouzey
2011-10-11
Moved to a more standard order of arguments (i.e. env followed by evar_map)
herbelin
2011-02-11
Update changelogs
glondu
2010-09-30
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
glondu
2010-07-22
Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).
herbelin
2010-06-29
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-14
Fixed commit 13125 (stricter check of induction args): an interpretation
herbelin
2010-06-13
Fixed a bug in pretty-printing "induction" and "destruct" due to a
herbelin
2010-05-13
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-04-14
Removing redundant internal variants of apply tactic and simplification of ML...
herbelin
2010-04-05
Added a function in typing.ml to solve evars of a constr w/o going back down ...
herbelin
2009-11-09
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-08
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-08-06
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-05-09
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
[next]