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-19
Attempt to improve error rendering in pattern-matching compilation (#5142).
Hugo Herbelin
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-18
[stm] Fix record field name clash.
Emilio Jesus Gallego Arias
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.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
2016-10-17
Fix bug #5023: JSON extraction doesn't generate "for xxx".
Pierre-Marie Pédrot
2016-10-16
Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".
Pierre-Marie Pédrot
2016-10-15
Fix bug #5145: Anomaly: index to an anonymous variable.
Pierre-Marie Pédrot
2016-10-15
Still a problem with debug auto printing.
Hugo Herbelin
2016-10-15
One more little bug in the output of "debug auto".
Hugo Herbelin
2016-10-14
Fix bug #5139: Anomalies should not be caught by || / try.
Pierre-Marie Pédrot
2016-10-14
Fixing printing of info_auto broken since 0091c528 (2014).
Hugo Herbelin
2016-10-14
Fixing English typography for colon.
Hugo Herbelin
2016-10-14
Using "simple apply" and "simple eapply" in the trace of auto.
Hugo Herbelin
2016-10-13
Completing reverting generalization and cleaning of the return clause inference.
Hugo Herbelin
2016-10-12
Remove dead code in Environ.
Pierre-Marie Pédrot
2016-10-12
Merge PR #224 into v8.6
Pierre-Marie Pédrot
2016-10-12
Merge PR #289 into v8.6.
Pierre-Marie Pédrot
2016-10-12
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
Tentatively preparing to add changes specific to v8.7 (see PR #275).
Hugo Herbelin
2016-10-12
Little addition to 6eede071 for consistency of style in OrdersFacts.v.
Hugo Herbelin
2016-10-12
Fixing a collision about the meta-variable ".." in recursive notations.
Hugo Herbelin
2016-10-12
Merge remote-tracking branch 'github/pr/286' into v8.5
Maxime Dénès
[next]