index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
Commit message (
Expand
)
Author
Age
...
|
*
|
Trying to circumvent hdiutil error 5341 by padding.
Maxime Dénès
2016-03-14
*
|
|
Removing an empty file detected by Luc Grateau.
Hugo Herbelin
2016-03-12
*
|
|
Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into aspi...
Hugo Herbelin
2016-03-09
|
\
\
\
*
|
|
|
Putting Tactic_debug just below Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
|
|
|
Moving Tactic_debug to tactics/ folder.
Pierre-Marie Pédrot
2016-03-06
*
|
|
|
Moving Ltac traces to Tacexpr and Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
|
|
|
Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.
Pierre-Marie Pédrot
2016-03-06
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
|
*
|
|
Fix a typo in dev/doc/changes.txt
Jason Gross
2016-03-04
*
|
|
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
|
|
*
|
|
Compile OS X binaries without native_compute support.
Maxime Dénès
2016-01-21
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
|
*
|
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
|
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
|
|
|
|
*
|
|
Fixing #4467 (continued).
Hugo Herbelin
2016-01-13
*
|
|
|
merge
Matej Kosik
2016-01-11
|
\
\
\
\
|
*
|
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-06
|
\
\
\
\
\
|
|
|
/
/
/
|
|
/
|
|
|
|
*
|
|
|
Fix order of files in mllib.
Maxime Dénès
2016-01-05
*
|
|
|
|
Simplification of grammar_prod_item type.
Pierre-Marie Pédrot
2016-01-02
*
|
|
|
|
Finer-grained types for toplevel values.
Pierre-Marie Pédrot
2015-12-21
*
|
|
|
|
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-12-21
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Tying the loop in tactic printing API.
Pierre-Marie Pédrot
2015-12-18
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
|
|
*
|
|
Fixing a minor problem in Makefile.build that was prevening "dev/printers.cma...
Matej Kosik
2015-12-07
|
*
|
|
Fix some typos.
Guillaume Melquiond
2015-12-07
*
|
|
|
Factorizing unsafe code by relying on the new Dyn module.
Pierre-Marie Pédrot
2015-12-05
*
|
|
|
Ensuring that documentation of mli code works in the presence of utf-8
Hugo Herbelin
2015-12-05
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
|
|
|
*
|
|
Update history of revisions.
Hugo Herbelin
2015-12-02
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
|
|
*
|
|
MacOS package script: do not fail if link to /Applications already exists.
Maxime Dénès
2015-11-18
|
*
|
|
Being more precise and faithful about the origin of the file reporting
Hugo Herbelin
2015-11-16
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-15
|
\
|
|
|
|
*
|
|
MacOS package script: do not fail if directory _dmg already exists.
Maxime Dénès
2015-11-13
|
*
|
|
Script building MacOS package.
Maxime Dénès
2015-11-12
|
|
*
|
Prehistory of Coq: move the bibliographic references to a dedicated section.
Arnaud Spiwack
2015-11-11
|
|
*
|
Prehistory of Coq: justification of the plain text.
Arnaud Spiwack
2015-11-11
|
|
*
|
Prehistory of Coq: consistency.
Arnaud Spiwack
2015-11-11
|
|
*
|
Prehistory of Coq: various corrections on English.
Arnaud Spiwack
2015-11-11
|
|
*
|
Prehistory of Coq: asciidoc conversion.
Arnaud Spiwack
2015-11-11
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
|
|
|
*
|
|
Fixing another instance of bug #3267 in eauto, this time in the
Hugo Herbelin
2015-10-29
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
|
|
|
/
/
|
/
|
|
|
*
|
Refine Gregory Malecha's patch on VM and universe polymorphism.
Maxime Dénès
2015-10-28
|
*
|
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
|
|
Type-safe Egramml.grammar_prod_item.
Pierre-Marie Pédrot
2015-10-27
[prev]
[next]