aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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
2016-09-30In <= 8.5 compat accept "Arguments f /" even if f has arguments (#5112)Enrico Tassi
2016-09-30Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimplEnrico Tassi
2016-09-30[pp] Remove duplicate color logger.Emilio Jesus Gallego Arias
2016-09-29Fix bug #4798: compat notations should not modify the parser.Pierre-Marie Pédrot
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-09-29Merge branch 'bug4723' into v8.6Matthieu Sozeau
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-29fix bug 3683 : adds references to the web site for the bug trackerYves Bertot
2016-09-29Fix bug #5011: Anomaly on [Existing Class].Pierre-Marie Pédrot
2016-09-29Cleanup API, making inference_hook optionalMatthieu Sozeau
2016-09-29Argument : assert does fail if no arg is given (fix #4864)Enrico Tassi
2016-09-29-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)Enrico Tassi
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu Sozeau
2016-09-27Merge remote-tracking branch 'github/pr/290' into trunkMaxime Dénès
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-268.7 now points to Current and 8.6 points to V8_6.Théo Zimmermann
2016-09-25The coqtop options -Q and -R do not affect the ML loadpath anymore.Pierre-Marie Pédrot
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 07:24:32 +0000