aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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-10Fixing #5133 (error reporting delayed).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-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.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-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-25The coqtop options -Q and -R do not affect the ML loadpath anymore.Pierre-Marie Pédrot
2016-09-22coqc -o now places .glob file near .vo fileEnrico Tassi
2016-09-19Fix warning when using Variables at toplevel.Maxime Dénès
2016-09-17Fix indentation of -profile-ltac in -helpJason Gross
2016-09-13coqc: print debug feedback coming from workersEnrico Tassi
2016-09-10Avoid putting a useless "toploop" directory in the ML search path if it does ...Guillaume Melquiond
2016-09-09Make it explicit when paths are added to the ML search paths.Guillaume Melquiond
2016-09-08Avoid canonizing the same paths over and over.Guillaume Melquiond
2016-08-30Fix #4941 - ~/.coqrc file confusing locationsMaxime Dénès
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-08-25Do not export an internal function in Namegen.Pierre-Marie Pédrot
2016-08-24Properly compute types for assumed section variables (bug #5035).Guillaume Melquiond
2016-08-24Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Pierre-Marie Pédrot
2016-08-24Merge PR #258: "Fix newline issues" into v8.6Pierre-Marie Pédrot
2016-08-23Arguments: give / after last ! error detection fixedEnrico Tassi
2016-08-23fix get_host_port error message (#4724)Enrico Tassi
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-20Fixing an anomaly in printing a unification error message.Hugo Herbelin