index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
CHANGES
Commit message (
Expand
)
Author
Age
*
Update CHANGES with inversion_sigma entry
Jason Gross
2017-06-30
*
Merge PR#774: [ide] Add route_id parameter to query call.
Maxime Dénès
2017-06-20
|
\
|
*
[ide] Add route_id parameter to query call.
Emilio Jesus Gallego Arias
2017-06-18
*
|
Document cumulativity for inductive types
Amin Timany
2017-06-16
|
/
*
BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)
Pierre Letouzey
2017-06-13
*
Merge PR#709: Bytecode compilation apart from 'make world', again
Maxime Dénès
2017-06-12
|
\
|
*
mention 'make world' without 'byte' in CHANGES + 2 minor suggestions
Pierre Letouzey
2017-06-01
*
|
Merge PR#449: make specialize smarter (bug 5370).
Maxime Dénès
2017-06-01
|
\
\
|
*
|
Tests for new specialize feature + CHANGES.
Pierre Courtieu
2017-05-31
|
|
/
*
/
Documentation for eassert, eenough, epose proof, eset, eremember, epose.
Hugo Herbelin
2017-05-30
|
/
*
Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings
Maxime Dénès
2017-05-25
|
\
*
\
Merge PR#406: coq makefile2
Maxime Dénès
2017-05-25
|
\
\
|
*
|
enters coq_makefile2
Enrico Tassi
2017-05-23
*
|
|
[vernac] Remove `Save thm id.` command.
Emilio Jesus Gallego Arias
2017-05-23
|
/
/
|
*
Clarifying the interpretation path for the "constr_with_binding" argument.
Hugo Herbelin
2017-05-22
|
/
*
Merge PR#457: Adding an even more compact goal hyps mode.
Maxime Dénès
2017-05-17
|
\
*
|
Aligning on standard layout of CHANGES.
Hugo Herbelin
2017-05-13
|
*
Documenting Printing Compact Contexts + CHANGES
Pierre Courtieu
2017-05-11
*
|
Tentative note in CHANGES about now applying βι while typing "match" branches.
Hugo Herbelin
2017-04-27
|
/
*
CHANGES entry for #545.
Maxime Dénès
2017-04-19
*
Merge PR#379: Introducing evar-insensitive constrs
Maxime Dénès
2017-04-11
|
\
|
*
Documenting the changes introduced by the EConstr branch.
Pierre-Marie Pédrot
2017-04-10
*
|
[camlpX] Enrico's changes to camlp4 removal.
Emilio Jesus Gallego Arias
2017-04-07
|
/
*
Merge PR#455: Farewell decl_mode
Maxime Dénès
2017-04-06
|
\
*
|
Document the changes to IZR.
Guillaume Melquiond
2017-03-22
|
*
Farewell decl_mode
Enrico Tassi
2017-03-07
*
|
CHANGES: choice over setoids and prop. ext.
Hugo Herbelin
2017-03-03
|
/
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-01-19
|
\
|
*
A few words in CHANGES.
Maxime Dénès
2016-12-07
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-30
|
\
|
|
*
Fix some documentation typos.
Guillaume Melquiond
2016-11-24
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
\
|
|
*
[doc] Mention XML protocol on changes.
Emilio Jesus Gallego Arias
2016-11-16
|
*
Remove the list of bug fixes from CHANGES.
Maxime Dénès
2016-11-14
|
*
Update CHANGES and credits for 8.6beta1.
Maxime Dénès
2016-11-10
|
*
Mention notypeclasses refine in CHANGES
Matthieu Sozeau
2016-11-07
|
*
CHANGES for this branch.
Matthieu Sozeau
2016-11-07
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-26
|
|
\
|
|
*
Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."
Maxime Dénès
2016-10-25
|
|
*
Update CHANGES.
Maxime Dénès
2016-10-25
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-12
|
\
|
|
*
|
|
Allocating a section in CHANGES for changes specific to 8.7.
Hugo Herbelin
2016-10-12
|
*
|
Tentatively preparing to add changes specific to v8.7 (see PR #275).
Hugo Herbelin
2016-10-12
|
/
/
*
|
Report about changes of semantics of auto as an ltac argument (see #4966).
Hugo Herbelin
2016-10-08
*
|
Remove the Set Verbose Compat option and turn the warning on by default.
Maxime Dénès
2016-10-06
*
|
Document change related to Keep Proof Equalities in CHANGES.
Maxime Dénès
2016-10-03
*
|
Being more informative about the change of behavior of "subst".
Hugo Herbelin
2016-09-29
*
|
Fix description of change in intro semantics.
Maxime Dénès
2016-09-21
*
|
Extending "contradiction" so that it recognizes statements such as "~x=x" or ...
Hugo Herbelin
2016-09-15
[next]