aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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
2016-09-22coqc -o now places .glob file near .vo fileEnrico Tassi
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-22Merge remote-tracking branch 'github/pr/283' into trunkMaxime Dénès
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-20Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
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-16Make the Coq codebase independent from Ltac-related code.Pierre-Marie Pédrot
2016-09-14Allowing to extend the Print Grammar command generically.Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
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-09-08Making Proof_global terminator generic in external tactics.Pierre-Marie Pédrot
2016-09-08Unplugging Tacexpr in several interface files.Pierre-Marie Pédrot
2016-09-08Making Vernacexpr independent from Tacexpr.Pierre-Marie Pédrot
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-09-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-08-30Fix #4941 - ~/.coqrc file confusing locationsMaxime Dénès
2016-08-30CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Matej Kosik
2016-08-30CLEANUP: using |> operator more consistentlyMatej Kosik
2016-08-29CLEANUP: taking advantage of "_ % _" operator to express function composition...Matej Kosik
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-08-25Merge remote-tracking branch 'v8.6' into trunkMatej Kosik
2016-08-25Do not export an internal function in Namegen.Pierre-Marie Pédrot
2016-08-25CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionMatej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 13:29:37 +0000