aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
* Add Unset Use Unif Heuristics in Compat/Coq85Gravatar Matthieu Sozeau2016-10-22
* Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
* Port fix for bugs 4763, 5149, previously 0b417c12eGravatar Matthieu Sozeau2016-10-22
* Adding a test for bug #3495.Gravatar Pierre-Marie Pédrot2016-10-21
* Oops, my bad, didn't expect a merge issue!Gravatar Matthieu Sozeau2016-10-21
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
|\
* | Adding a primitive to recover the set of keywords from the lexer.Gravatar Pierre-Marie Pédrot2016-10-21
| * Revert "unification.ml: fix for bug #4763, unif regression"Gravatar Maxime Dénès2016-10-21
* | Merge branch 'fixminimization' into v8.6Gravatar Matthieu Sozeau2016-10-21
|\ \
* | | Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Gravatar Matthieu Sozeau2016-10-21
| * | Remove no longer exported debug printerGravatar Matthieu Sozeau2016-10-21
| | * Merge remote-tracking branch 'github/pr/328' into v8.5Gravatar Maxime Dénès2016-10-21
| | |\
* | | \ Merge remote-tracking branch 'github/pr/233' into v8.6Gravatar Maxime Dénès2016-10-21
|\ \ \ \
| | | * | Adding dependency of the test-suite subsystems in prerequisite (fixing #5150).Gravatar Hugo Herbelin2016-10-20
| | | * | A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).Gravatar Hugo Herbelin2016-10-20
| | * | | Cleanup code according to comments.Gravatar Matthieu Sozeau2016-10-20
| | * | | Fix minimization to be insensitive to redundant arcs.Gravatar Matthieu Sozeau2016-10-20
| |/ / / |/| | |
* | | | Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-10-20
|\ \ \ \
| * | | | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-10-20
| | * | | [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
| |/ / / |/| | |
* | | | Merge remote-tracking branch 'github/printcandidates' into v8.6Gravatar Matthieu Sozeau2016-10-20
|\ \ \ \
| * | | | Refine printing of pending unification constraintsGravatar Matthieu Sozeau2016-10-20
|/ / / /
* | | | Test for variant of #5142 (good error message on pattern-matching failure).Gravatar Hugo Herbelin2016-10-19
* | | | Attempt to improve error rendering in pattern-matching compilation (#5142).Gravatar Hugo Herbelin2016-10-19
* | | | More comments in VM.Gravatar Maxime Dénès2016-10-19
* | | | Error Resiliency: more conservative default (only curly braces)Gravatar Enrico Tassi2016-10-19
| | | * Change the order of arguments of fig2dev.Gravatar Théo Zimmermann2016-10-19
| | |/
* | | [stm] Fix record field name clash.Gravatar Emilio Jesus Gallego Arias2016-10-18
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-18
|\ \ \ | | |/ | |/|
| * | Removing output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-18
* | | Quick fix to unification regression #4955.Gravatar Hugo Herbelin2016-10-17
* | | Extra warning about unicode character of unknown status following an ident.Gravatar Hugo Herbelin2016-10-17
* | | Fixing a few other inconsistencies with notations.Gravatar Hugo Herbelin2016-10-17
* | | Stopping warning on unrecognized unicode character in notation (fixing #5136).Gravatar Hugo Herbelin2016-10-17
* | | [toplevel] Remove undocumented "just_parsing" flag.Gravatar Emilio Jesus Gallego Arias2016-10-17
* | | [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
* | | Vernac.ml: inlining read_vernac_file within load_vernac.Gravatar Hugo Herbelin2016-10-17
* | | Grouping checks about commands together.Gravatar Hugo Herbelin2016-10-17
* | | Vernac.ml: parenthesizing a side-effect.Gravatar Hugo Herbelin2016-10-17
* | | Factorizing two instances of load_vernac.Gravatar Hugo Herbelin2016-10-17
* | | Passing chan_beautify functionally rather than by side-effect.Gravatar Hugo Herbelin2016-10-17
* | | Applying Emilio's suggestion to simplify type of eval_expr.Gravatar Hugo Herbelin2016-10-17
* | | More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
* | | Removing export of location_table outside of cLexer.Gravatar Hugo Herbelin2016-10-17
* | | Fix compilation with camlp4 broken in 8a8caba3.Gravatar Hugo Herbelin2016-10-17
| * | Fixing to #3209 (Not_found due to an occur-check cycle).Gravatar Hugo Herbelin2016-10-17
| * | Fixing a missing constraint in consider_remaining_unif_constraints.Gravatar Hugo Herbelin2016-10-17
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\| |
* | | Fix output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-17