aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
* [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
* Fix bug in warnings: -w foo was silent when foo did not exist.Gravatar Maxime Dénès2016-11-14
* Do not mention "none" in warnings doc, as it is there for compatibility.Gravatar Maxime Dénès2016-11-14
* 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
* | | 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
|\ \ \ \
| | | | * 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
| |_|/ |/| |
* | | [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 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
|\ \
* | | 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
* | | 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.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-05
|\ \ \ | | |/ | |/|
* | | Fix a bug of Mltop.declare_cache_object.Gravatar Pierre-Marie Pédrot2016-10-05
* | | Quick fix to #4595 (making notations containing "ltac:" unused for printing).Gravatar Hugo Herbelin2016-10-04
* | | Merge remote-tracking branch 'github/pr/305' into v8.6Gravatar Maxime Dénès2016-10-04
|\ \ \
| | * | Fixing #4970 (confusion between special "{" and non special "{{" in notations).Gravatar Hugo Herbelin2016-10-03
* | | | Fix bug #5069: Scheme Equality gives anomalies in sections.Gravatar Pierre-Marie Pédrot2016-10-02