index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Merge PR#355: Remove unused feedback_content: Goals
Maxime Dénès
2017-01-30
|
\
*
|
Adding a printer for Proof.proof reflecting the focusing layout.
Hugo Herbelin
2017-01-26
*
|
Adding a new evar source to remember the name of evars which were
Hugo Herbelin
2017-01-22
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-01-19
|
\
\
|
*
|
Mapping named_context_val preserves sharing when possible.
Pierre-Marie Pédrot
2017-01-17
|
*
|
STM: fix run-time classification of VernacInstance (fix #5313)
Enrico Tassi
2017-01-17
|
*
|
Fixing (part of) #5303 (clarifications around Record/Structure/Variant).
Hugo Herbelin
2017-01-16
|
*
|
Fix race condition in STM DAG generation (in debug mode).
Maxime Dénès
2017-01-13
|
*
|
Properly remove aux files in subdirectories (bug #5089).
Erik Martin-Dorel
2017-01-13
|
*
|
Fix broken .aux machinery.
Guillaume Melquiond
2017-01-13
|
*
|
Fix configure crash on some version strings of camlp5, e.g. "6.18-exp" (bug #...
Guillaume Melquiond
2017-01-12
*
|
|
Avoid using the deprecated Scanf.fscanf function.
Maxime Dénès
2017-01-09
*
|
|
OCaml's -dtypes flag is deprecated and replaced by -annot.
Maxime Dénès
2017-01-09
*
|
|
Relax required OCaml to 4.02.1.
Maxime Dénès
2017-01-09
*
|
|
Merge remote-tracking branch 'github/pr/350' into trunk
Maxime Dénès
2017-01-09
|
\
\
\
|
|
*
|
Fixing another inconsistency when looking for camlp5o when camlp5dir is given.
Hugo Herbelin
2017-01-04
|
|
*
|
Fix some typos in tutorial (bug #5294).
Guillaume Melquiond
2016-12-28
|
|
*
|
Handle application of a primitive projection to a not yet evaluated cofixpoin...
Guillaume Melquiond
2016-12-23
*
|
|
|
Fixing #5277 (Scheme Equality not robust wrt choice of names).
Hugo Herbelin
2016-12-22
*
|
|
|
Fixing injection in the presence of let-in in constructors.
Hugo Herbelin
2016-12-22
*
|
|
|
Merge remote-tracking branch 'github/pr/172' into trunk
Maxime Dénès
2016-12-19
|
\
\
\
\
|
|
|
*
|
Avoid concurrent runs when producing html documentation (bug #5269).
Guillaume Melquiond
2016-12-19
*
|
|
|
|
Merge remote-tracking branch 'github/pr/351' into trunk
Maxime Dénès
2016-12-19
|
\
\
\
\
\
*
\
\
\
\
\
Merge remote-tracking branch 'github/pr/363' into trunk
Maxime Dénès
2016-12-19
|
\
\
\
\
\
\
*
|
|
|
|
|
|
Fix a typo in Hurkens.v comment
Jason Gross
2016-12-19
*
|
|
|
|
|
|
Bump required OCaml version to 4.02.3.
Maxime Dénès
2016-12-19
*
|
|
|
|
|
|
Use Pp.quote in string options.
Maxime Dénès
2016-12-19
|
|
|
|
|
*
|
Fix incorrect documentation that prevents successful compilation (bug #5265).
Guillaume Melquiond
2016-12-16
|
|
|
|
|
*
|
Set version to 8.6 in configure.
Maxime Dénès
2016-12-08
|
|
|
|
|
*
|
Windows build scripts for 8.6 final.
Maxime Dénès
2016-12-08
|
|
|
|
|
*
|
Fix paths in 32-bit windows build scripts.
Maxime Dénès
2016-12-08
|
|
|
|
|
*
|
Commit bumping the version number was partial...
Maxime Dénès
2016-12-07
|
|
|
|
|
*
|
Add bat files for 8.6rc1 build.
Maxime Dénès
2016-12-07
|
|
|
|
|
*
|
Add bat files for 8.6beta1 build.
Maxime Dénès
2016-12-07
|
|
|
|
|
*
|
Set version number to 8.6rc1.
Maxime Dénès
2016-12-07
|
|
|
|
|
*
|
A few words in CHANGES.
Maxime Dénès
2016-12-07
|
|
|
|
|
*
|
ssrmatching: fix iter_constr_LR iterator wrt Proj
Enrico Tassi
2016-12-07
*
|
|
|
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-07
|
\
\
\
\
\
\
\
|
|
|
_
|
_
|
_
|
/
/
|
|
/
|
|
|
|
|
|
*
|
|
|
|
|
Fix #5248 - test-suite fails in 8.6beta1
Maxime Dénès
2016-12-06
|
*
|
|
|
|
|
Fix broken documentation in presence of \zeroone{... \tt ...}.
Guillaume Melquiond
2016-12-06
|
*
|
|
|
|
|
Update documentation (bugs #5246 and #5251).
Guillaume Melquiond
2016-12-06
|
*
|
|
|
|
|
Merge remote-tracking branch 'github/pr/387' into v8.6
Maxime Dénès
2016-12-06
|
|
\
\
\
\
\
\
|
*
\
\
\
\
\
\
Merge remote-tracking branch 'github/pr/389' into v8.6
Maxime Dénès
2016-12-06
|
|
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
Change module for Coq loop
Paul Steckler
2016-12-05
|
|
*
|
|
|
|
|
|
the -byte option is deprecated
Paul Steckler
2016-12-05
|
|
/
/
/
/
/
/
/
|
|
*
|
|
|
|
|
ssrmatching: handle primite projections (fix: #5247)
Enrico Tassi
2016-12-05
|
*
|
|
|
|
|
|
Compute dependency of C files only in kernel/byterun.
Maxime Dénès
2016-12-05
|
|
/
/
/
/
/
/
|
*
|
|
|
|
|
Merge remote-tracking branch 'github/pr/366' into v8.6
Maxime Dénès
2016-12-04
|
|
\
\
\
\
\
\
|
*
\
\
\
\
\
\
Merge remote-tracking branch 'github/pr/378' into v8.6
Maxime Dénès
2016-12-04
|
|
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
Fix test-suite after change in "context" printing.
Maxime Dénès
2016-12-02
[next]
Maxime Dénès
Hugo Herbelin
Pierre-Marie Pédrot
Enrico Tassi
Erik Martin-Dorel
Guillaume Melquiond
Jason Gross
Paul Steckler