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
*
Mention bug 3199 fix as a source of incompatibilities.
Matthieu Sozeau
2015-10-21
*
Bug #3956 is fixed.
Matthieu Sozeau
2015-10-21
*
Fixed (and changed) infoH.
Pierre Courtieu
2015-10-21
*
Fix lemma-overloading
Matthieu Sozeau
2015-10-20
*
Do occur-check w.r.t existential's types also when instantiating an evar.
Matthieu Sozeau
2015-10-19
*
Categorizing debug messages as such + NonLogical uses loggers.
Pierre Courtieu
2015-10-19
*
Test for #4372 (anomaly in inversion in the presence of fake dependency).
Hugo Herbelin
2015-10-19
*
Turning anomaly into error for #4372 (weakness of inversion in the
Hugo Herbelin
2015-10-19
*
Partly fixes #3225. Removed some old experimental stuff in funind.
Pierre Courtieu
2015-10-19
*
Fixed #4274, bad formatting of messages in emacs mode.
Pierre Courtieu
2015-10-19
*
Documenting the option "Strict Universe Declaration" in CHANGES.
Pierre-Marie Pédrot
2015-10-19
*
Miscellaneous typos, spacing, US spelling in comments or variable names.
Hugo Herbelin
2015-10-18
*
Using "__" rather than this unelegant arbitrary "A" for the name of variables...
Hugo Herbelin
2015-10-18
*
Reference Manual: Applying standard style recommendation about not
Hugo Herbelin
2015-10-18
*
Fixing #4198 (continued): not matching within the inner lambdas/let-ins
Hugo Herbelin
2015-10-18
*
Using appropriate lambda decomposition function counting let-ins when
Hugo Herbelin
2015-10-18
*
Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,
Hugo Herbelin
2015-10-18
*
Lemmas accept the Local flag.
Pierre-Marie Pédrot
2015-10-17
*
Test for bug #4325.
Pierre-Marie Pédrot
2015-10-17
*
Generalize fix for auto from PMP to eauto and typeclasses eauto.
Matthieu Sozeau
2015-10-16
*
Remove left2right reference from the kernel.
Maxime Dénès
2015-10-16
*
Merge hint lists instead of appending them. (Fix bug #3199)
Guillaume Melquiond
2015-10-16
*
Avoid dependency of the pretyper on C code.
Maxime Dénès
2015-10-15
*
Test file for #4346: Set is no longer of type Type
Maxime Dénès
2015-10-15
*
Fix #4346 2/2: VM casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
*
Fix #4346 1/2: native casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
*
Warn user when bytecode compilation fails.
Maxime Dénès
2015-10-15
*
Remove now useless exception handler in default conversion.
Maxime Dénès
2015-10-15
*
Fix detection of ties in oracle_order.
Guillaume Melquiond
2015-10-15
*
Reverting modifications in dev/top_printers pushed mistakenly.
Pierre-Marie Pédrot
2015-10-14
*
Fixing perfomance issue of auto hints induced by universes.
Pierre-Marie Pédrot
2015-10-14
*
Fix LemmaOverloading
Matthieu Sozeau
2015-10-14
*
Occur-check in evar_define was not strong enough.
Matthieu Sozeau
2015-10-14
*
Fix constr_matching when a match is found in the head of a case construct
Matthieu Sozeau
2015-10-14
*
When typechecking a lemma statement, try to resolve typeclasses before
Matthieu Sozeau
2015-10-14
*
Univs: inductives, remove unneeded test
Matthieu Sozeau
2015-10-14
*
Temporary fix: kernel conversion needs to ignore l2r flag.
Maxime Dénès
2015-10-14
*
Exporting the original unprocessed hint in the hint running function.
Pierre-Marie Pédrot
2015-10-14
*
Fixing evarmap implementation.
Pierre-Marie Pédrot
2015-10-14
*
Remove reference to default conversion function inside the kernel.
Maxime Dénès
2015-10-14
*
Remove -vm flag of coqtop.
Maxime Dénès
2015-10-14
*
Remove unused infos structure in VM.
Maxime Dénès
2015-10-14
*
Fixing bug #4367: Wrong error message in unification.
Pierre-Marie Pédrot
2015-10-14
*
Make interpreter of PROJ simpler by not using the stack.
Guillaume Melquiond
2015-10-14
*
Remove some unused variables.
Guillaume Melquiond
2015-10-14
*
Fix some typos.
Guillaume Melquiond
2015-10-14
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Remove code that was already commented out.
Maxime Dénès
2015-10-12
*
Univs: be more restrictive for template polymorphic constants: only
Matthieu Sozeau
2015-10-12
*
Fix Definition id := Eval <redexpr> in by passing the right universe
Matthieu Sozeau
2015-10-12
[next]