index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2016-10-20
CLEANUP: Namegen.to_avoid
Matej Kosik
2016-10-20
Merge remote-tracking branch 'github/printcandidates' into v8.6
Matthieu Sozeau
2016-10-20
Refine printing of pending unification constraints
Matthieu Sozeau
2016-10-19
Documenting Hint Resolve -> and <- variants.
Théo Zimmermann
2016-10-19
Test for variant of #5142 (good error message on pattern-matching failure).
Hugo Herbelin
2016-10-19
Attempt to improve error rendering in pattern-matching compilation (#5142).
Hugo Herbelin
2016-10-19
enriching ".gitignore"
Matej Kosik
2016-10-19
More comments in VM.
Maxime Dénès
2016-10-19
Error Resiliency: more conservative default (only curly braces)
Enrico Tassi
2016-10-19
Making the doc of auto hints more precise.
Théo Zimmermann
2016-10-19
COMMENT: was added to "Nameops.increment_suffix".
Matej Kosik
2016-10-19
CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".
Matej Kosik
2016-10-19
Converting certain "order-only" (Makefile) dependencies to regular dependencies.
Matej Kosik
2016-10-19
Change the order of arguments of fig2dev.
Théo Zimmermann
2016-10-18
[pp] Use more convenient pp API in ssrmatching
Emilio Jesus Gallego Arias
2016-10-18
[pp] Try to properly tag error messages in cError.
Emilio Jesus Gallego Arias
2016-10-18
[pp] Add tagging function to all low-level printing calls.
Emilio Jesus Gallego Arias
2016-10-18
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-18
Extending the doc with a general summary of auto variants.
Théo Zimmermann
2016-10-18
Document info_auto.
Théo Zimmermann
2016-10-18
[stm] Fix record field name clash.
Emilio Jesus Gallego Arias
2016-10-18
Improve the documentation of eauto.
Théo Zimmermann
2016-10-18
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-18
Removing output test for module qualification.
Pierre-Marie Pédrot
2016-10-17
Quick fix to unification regression #4955.
Hugo Herbelin
2016-10-17
Extra warning about unicode character of unknown status following an ident.
Hugo Herbelin
2016-10-17
Fixing a few other inconsistencies with notations.
Hugo Herbelin
2016-10-17
Stopping warning on unrecognized unicode character in notation (fixing #5136).
Hugo Herbelin
2016-10-17
[toplevel] Remove undocumented "just_parsing" flag.
Emilio Jesus Gallego Arias
2016-10-17
[toplevel] Remove duplicate beautify flags.
Emilio Jesus Gallego Arias
2016-10-17
Vernac.ml: inlining read_vernac_file within load_vernac.
Hugo Herbelin
2016-10-17
Grouping checks about commands together.
Hugo Herbelin
2016-10-17
Vernac.ml: parenthesizing a side-effect.
Hugo Herbelin
2016-10-17
Factorizing two instances of load_vernac.
Hugo Herbelin
2016-10-17
Passing chan_beautify functionally rather than by side-effect.
Hugo Herbelin
2016-10-17
Applying Emilio's suggestion to simplify type of eval_expr.
Hugo Herbelin
2016-10-17
More on making the lexer more functional (continuing b8ae2de5 and
Hugo Herbelin
2016-10-17
Removing export of location_table outside of cLexer.
Hugo Herbelin
2016-10-17
Fix compilation with camlp4 broken in 8a8caba3.
Hugo Herbelin
2016-10-17
Fixing to #3209 (Not_found due to an occur-check cycle).
Hugo Herbelin
2016-10-17
Fixing a missing constraint in consider_remaining_unif_constraints.
Hugo Herbelin
2016-10-17
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-17
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-17
Fix output test for module qualification.
Pierre-Marie Pédrot
2016-10-17
Fix previous commit.
Pierre-Marie Pédrot
2016-10-17
Merge PR #300 into v8.6
Pierre-Marie Pédrot
2016-10-17
Example illustrating non-local inference of the default type of impossible br...
Hugo Herbelin
2016-10-17
Merge PR #310 into v8.5
Pierre-Marie Pédrot
2016-10-17
Merge PR #310 into v8.6
Pierre-Marie Pédrot
2016-10-17
Test for bug #4874.
Pierre-Marie Pédrot
[prev]
[next]