aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
...
| | | * Sort search results by relevanceGravatar Arnaud Spiwack2016-11-07
| |_|/ |/| |
| * | Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \
| | * | Fixes to compile with ocaml 4.01Gravatar Matthieu Sozeau2016-11-07
| * | | Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \ \
| * | | | Improve formatting of a message in [Arguments].Gravatar Maxime Dénès2016-11-07
| * | | | Fix #5181: [Arguments] no longer correctly checks the length of arguments listsGravatar Maxime Dénès2016-11-07
| * | | | Fix #5182: "Arguments names must be distinct." is bogus and underinformativeGravatar Maxime Dénès2016-11-07
| * | | | Not using style tags when translating/beautifying a file.Gravatar Hugo Herbelin2016-11-05
| * | | | Quick fix of tactic parsing while Load-ing in coqide.Gravatar Hugo Herbelin2016-11-04
| * | | | Add documentation for [Set Warnings] and the -w option.Gravatar Cyprien Mangin2016-11-04
| | | * | Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| * | | | Fix various shortcomings of the warnings infrastructure.Gravatar Maxime Dénès2016-11-02
* | | | | Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| | | |
| * | | | Removing dead code.Gravatar Hugo Herbelin2016-10-29
| | |/ / | |/| |
| * | | Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ \
| * \ \ \ Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ \ \
| | * | | | Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
| * | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\ \ \ \ \ | | | |_|_|/ | | |/| | |
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | | | |
| | | | | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |_|_|/ | |/| | |
| | * | | Fix a bug in error printing of unif constraintsGravatar Matthieu Sozeau2016-10-22
| * | | | [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
| | | | * [pp] Add tagging function to all low-level printing calls.Gravatar Emilio Jesus Gallego Arias2016-10-18
| | |_|/ | |/| |
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\| | |
| * | | [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
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\| | |
| * | | Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".Gravatar Pierre-Marie Pédrot2016-10-16
| | |/ | |/|
| * | Merge PR #224 into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
| |\ \
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| | |
| * | | Fixing #5133 (error reporting delayed).Gravatar Hugo Herbelin2016-10-10
| | | * A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).Gravatar Hugo Herbelin2016-10-09
| * | | Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
| * | | Attaching all extra imperative components of the lexer/parser state toGravatar Hugo Herbelin2016-10-09
| * | | Fixing beautification to file.Gravatar Hugo Herbelin2016-10-09
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\| | |
| * | | Fix bug #5125: Bad error message when attempting to use where with Class.Gravatar Pierre-Marie Pédrot2016-10-07
| * | | Remove the -no-compat-notations flag.Gravatar Maxime Dénès2016-10-06
| * | | Remove the Set Verbose Compat option and turn the warning on by default.Gravatar Maxime Dénès2016-10-06
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-05
| |\ \ \ | | | |/ | | |/|