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
*
Splitting ML tactics in one function per grammar entry.
Pierre-Marie Pédrot
2015-01-23
*
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-01-23
|
\
|
*
Extraction: fix #3629.
Maxime Dénès
2015-01-23
|
*
Add the possibility of defining opaque terms with program.
mlasson
2015-01-21
|
*
Reference Manual/Credits: expand the paragraph on the new proof engine to mat...
Arnaud Spiwack
2015-01-21
|
*
Reference Manual/Credits: native compute is a major contribution.
Arnaud Spiwack
2015-01-21
|
*
Reference manual/Credits: populate the "various smaller-scale improvements" p...
Arnaud Spiwack
2015-01-21
|
*
Reference Manual/Credits: remove a duplicate.
Arnaud Spiwack
2015-01-21
|
*
Reference manual: pass over the credit section for English.
Arnaud Spiwack
2015-01-21
|
*
Reference manual: fix typo in doc of [tryif/then/else].
Arnaud Spiwack
2015-01-21
*
|
Embedding the index of the ML tactic entry in the Tacexpr AST.
Pierre-Marie Pédrot
2015-01-21
|
*
Fix a critical bug in machine arithmetic for native compiler.
Maxime Dénès
2015-01-20
*
|
Making unification of LetIn's expressions more consistent (see #3920).
Hugo Herbelin
2015-01-19
|
*
Making unification of LetIn's expressions more consistent (see #3920).
Hugo Herbelin
2015-01-19
|
*
Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was
Maxime Dénès
2015-01-18
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-01-17
|
\
|
|
*
Remove dead code.
Maxime Dénès
2015-01-17
|
*
Fix #3379, now that Require inside modules is allowed again.
Maxime Dénès
2015-01-17
*
|
Merge branch '8.5' into trunk
Matthieu Sozeau
2015-01-18
|
\
|
*
|
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-18
*
|
Univs: Complete documentation in refman.
Matthieu Sozeau
2015-01-18
*
|
Partially revert "Forbid Require inside interactive modules and module types."
Maxime Dénès
2015-01-18
*
|
Revert "Adapting two files from test-suite to now forbidden Require's in modu...
Maxime Dénès
2015-01-18
*
|
Revert "Update test for #3363 now that Require is forbidden inside modules."
Maxime Dénès
2015-01-18
*
|
Revert "Fix files in test-suite having to do with Require inside modules."
Maxime Dénès
2015-01-18
*
|
Avoid compilation warning... might not be the best fix though.
Matthieu Sozeau
2015-01-18
*
|
Univs: Fix alias computation for VMs, computation of normal form of
Matthieu Sozeau
2015-01-18
*
|
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-18
*
|
coq_makefile: install also .v and .glob
Enrico Tassi
2015-01-18
*
|
Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"
Matthieu Sozeau
2015-01-18
*
|
vm_printers: fix compilation
Enrico Tassi
2015-01-18
*
|
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-18
*
|
Minor fixes to the refman credits to be continued.
Matthieu Sozeau
2015-01-18
*
|
Move explanations about primitive projections to the manual.
Matthieu Sozeau
2015-01-18
*
|
Add a (by default deactivated) option to force typeclass resolution to
Matthieu Sozeau
2015-01-18
*
|
Expand Credits for 8.5 and doc on universes
Matthieu Sozeau
2015-01-18
*
|
Remove typeclass opaque directive, some proofs in the stdlib rely on it being...
Matthieu Sozeau
2015-01-18
*
|
Optionally allow eta-conversion during unification for type classes.
Matthieu Sozeau
2015-01-18
*
|
Update header of CHANGES.
Maxime Dénès
2015-01-18
|
*
There was one more universe needed due to the use of now non-universe-polymor...
Matthieu Sozeau
2015-01-18
|
*
Back to 4 expected universes.
Matthieu Sozeau
2015-01-17
|
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
|
*
Univs: Complete documentation in refman.
Matthieu Sozeau
2015-01-17
|
*
Partially revert "Forbid Require inside interactive modules and module types."
Maxime Dénès
2015-01-17
|
*
Revert "Adapting two files from test-suite to now forbidden Require's in modu...
Maxime Dénès
2015-01-17
|
*
Revert "Update test for #3363 now that Require is forbidden inside modules."
Maxime Dénès
2015-01-17
|
*
Revert "Fix files in test-suite having to do with Require inside modules."
Maxime Dénès
2015-01-17
|
*
Avoid compilation warning... might not be the best fix though.
Matthieu Sozeau
2015-01-17
|
*
Univs: Fix alias computation for VMs, computation of normal form of
Matthieu Sozeau
2015-01-17
|
*
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-17
[next]