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
...
*
Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
Pierre-Marie Pédrot
2016-02-17
*
Do not give a name to anonymous evars anymore. See bug #4547.
Pierre-Marie Pédrot
2016-02-13
*
STM: always stock in vio files the first node (state) of a proof
Enrico Tassi
2016-02-10
*
STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530
Enrico Tassi
2016-02-10
*
Don't fail fatally if PATH is not set.
Emilio Jesus Gallego Arias
2016-02-10
*
Improving error message with missing patterns in the presence of
Hugo Herbelin
2016-02-08
*
Optimizing the universes_of_constr_function.
Pierre-Marie Pédrot
2016-02-03
*
Optimizing the computation of frozen evars.
Pierre-Marie Pédrot
2016-02-03
*
Opacifying the type of evar naming structure in Evd.
Pierre-Marie Pédrot
2016-02-03
*
More compact representation for evar resolvability flag.
Pierre-Marie Pédrot
2016-02-03
*
Fix bug #4537: Coq 8.5 is slower in typeclass resolution.
Pierre-Marie Pédrot
2016-01-27
*
Fixing bde12b70 about reporting ill-formed constructor.
Hugo Herbelin
2016-01-26
*
Tentative fix for bug #4522: Incorrect "Warning..." on windows.
Pierre-Marie Pédrot
2016-01-24
*
Fixing bug #4373: coqdep does not know about .vio files.
Pierre-Marie Pédrot
2016-01-24
*
Fixing bug #3826: "Incompatible module types" is uninformative.
Pierre-Marie Pédrot
2016-01-24
*
Adding a test for bug #4378.
Pierre-Marie Pédrot
2016-01-24
*
Fixing bug #4495: Failed assertion in metasyntax.ml.
Pierre-Marie Pédrot
2016-01-24
*
Fixing bug #4511: evar tactic can create non-typed evars.
Pierre-Marie Pédrot
2016-01-24
*
Fix bug #4503: mixing universe polymorphic and monomorphic
Matthieu Sozeau
2016-01-23
*
Fix bug #4519: oops, global shadowed local universe level bindings.
Matthieu Sozeau
2016-01-23
*
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
*
Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form
Matthieu Sozeau
2016-01-23
*
Restore warnings produced by the interpretation of the command line
Hugo Herbelin
2016-01-22
*
Compile OS X binaries without native_compute support.
Maxime Dénès
2016-01-21
*
Update cic.mli MD5 after header update.
Maxime Dénès
2016-01-20
*
Update version number in configure.
Maxime Dénès
2016-01-20
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.
Maxime Dénès
2016-01-20
*
Documenting Set Bullet Behavior.
Hugo Herbelin
2016-01-20
*
Clarifying the documentation of tactics "cbv" and "lazy".
Hugo Herbelin
2016-01-20
*
Fixing Not_found on unknown bullet behavior.
Hugo Herbelin
2016-01-20
*
Fix bug #4420: check_types was losing universe constraints.
Matthieu Sozeau
2016-01-19
*
Thanks Hugo, but let's remain factual.
Maxime Dénès
2016-01-15
*
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
Minor edits in output of coqdep --help.
Maxime Dénès
2016-01-15
*
Fix #4408.
Pierre Courtieu
2016-01-15
*
Partially fixing #4408: coqdep --help is up to date.
Pierre Courtieu
2016-01-15
*
MMaps: remove it from final 8.5 release, since this new library isn't mature ...
Pierre Letouzey
2016-01-13
*
Fixing success of test for #3848 after move to directory "closed".
Hugo Herbelin
2016-01-13
*
Fixing #4467 (continued).
Hugo Herbelin
2016-01-13
*
Fixing #4467 (missing shadowing of variables in cases pattern).
Hugo Herbelin
2016-01-12
*
Fixing #4256 and #4484 (changes in evar-evar resolution made that new
Hugo Herbelin
2016-01-12
*
Reporting about the new tactical unshelve.
Hugo Herbelin
2016-01-12
*
Extend last commit: keyed unification uses full conversions on the applied co...
Matthieu Sozeau
2016-01-12
*
Extend Keyed Unification tests with the one from R. Krebbers.
Matthieu Sozeau
2016-01-12
*
Fix essential bug in new Keyed Unification mode reported by R. Krebbers.
Matthieu Sozeau
2016-01-12
*
Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.
Hugo Herbelin
2016-01-12
*
Documenting dtauto and dintuition.
Hugo Herbelin
2016-01-12
*
Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".
Hugo Herbelin
2016-01-12
*
Documenting option 'Set Bracketing Last Introduction Pattern'.
Hugo Herbelin
2016-01-12
[prev]
[next]