aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-29Removing dead code.Hugo Herbelin
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/337' into v8.6Maxime Dénès
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-22Fix a bug in error printing of unif constraintsMatthieu Sozeau
2016-10-20[search] Don't build intermediate lists in search.Emilio Jesus Gallego Arias
2016-10-18[pp] Add tagging function to all low-level printing calls.Emilio Jesus Gallego Arias
2016-10-18Merge branch 'v8.6'Pierre-Marie Pédrot
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-17Vernac.ml: inlining read_vernac_file within load_vernac.Hugo Herbelin
2016-10-17Grouping checks about commands together.Hugo Herbelin
2016-10-17Vernac.ml: parenthesizing a side-effect.Hugo Herbelin
2016-10-17Factorizing two instances of load_vernac.Hugo Herbelin
2016-10-17Passing chan_beautify functionally rather than by side-effect.Hugo Herbelin
2016-10-17Applying Emilio's suggestion to simplify type of eval_expr.Hugo Herbelin
2016-10-17More on making the lexer more functional (continuing b8ae2de5 andHugo Herbelin
2016-10-17Removing export of location_table outside of cLexer.Hugo Herbelin
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-16Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".Pierre-Marie Pédrot
2016-10-12Merge PR #224 into v8.6Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-10Fixing #5133 (error reporting delayed).Hugo Herbelin
2016-10-09A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).Hugo Herbelin
2016-10-09Moving Pp.comments to CLexer so that Pp is purer (no more side-effectHugo Herbelin
2016-10-09Attaching all extra imperative components of the lexer/parser state toHugo Herbelin
2016-10-09Fixing beautification to file.Hugo Herbelin
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-07Fix bug #5125: Bad error message when attempting to use where with Class.Pierre-Marie Pédrot
2016-10-06Remove the -no-compat-notations flag.Maxime Dénès
2016-10-06Remove the Set Verbose Compat option and turn the warning on by default.Maxime Dénès
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-05Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-05Fix a bug of Mltop.declare_cache_object.Pierre-Marie Pédrot
2016-10-04Quick fix to #4595 (making notations containing "ltac:" unused for printing).Hugo Herbelin
2016-10-04Merge remote-tracking branch 'github/pr/305' into v8.6Maxime Dénès
2016-10-03Fixing #4970 (confusion between special "{" and non special "{{" in notations).Hugo Herbelin
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-02Fix bug #5069: Scheme Equality gives anomalies in sections.Pierre-Marie Pédrot
2016-10-01Speed up the Search commands.Guillaume Melquiond
2016-10-01Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Guillaume Melquiond
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
2016-09-30Merge remote-tracking branch 'github/pr/281' into v8.6Maxime Dénès