aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-12-04Merge remote-tracking branch 'github/pr/378' into v8.6Maxime Dénès
2016-12-02Fix test-suite after change in "context" printing.Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/377' into v8.6Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/372' into v8.6Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/368' into v8.6Maxime Dénès
2016-12-02Merge branch 'pr/367' into v8.6Maxime Dénès
2016-12-02Fixing lexing of strings in comments for beautifier.Hugo Herbelin
2016-12-02Fixing printing of "ltac:" in tactics after surrounding parenthesesHugo Herbelin
2016-12-02Comment on universe handling in ParametersMatthieu Sozeau
2016-12-02Univs: fix bug #5188Matthieu Sozeau
2016-12-02Merge remote-tracking branch 'github/pr/381' into v8.6Maxime Dénès
2016-12-02Fix #5242 - Dubious unsilenceable warning on invalid identifierMaxime Dénès
2016-12-02Fixing printing of "Set Warnings Append".Hugo Herbelin
2016-12-02Fixing space in printing "Context".Hugo Herbelin
2016-12-02Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-12-02Fixing space in printing several list of implicit arguments.Hugo Herbelin
2016-12-02Fixing printing of "only parsing" in abbreviations.Hugo Herbelin
2016-12-02Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
2016-12-02More on fixing #5098 (preserving printing of "in hyp").Hugo Herbelin
2016-12-02Merge remote-tracking branch 'github/pr/380' into v8.6Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/369' into v8.6Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/371' into v8.6Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/364' into v8.6Maxime Dénès
2016-12-02Merge remote-tracking branch 'github/pr/382' into v8.6Maxime Dénès
2016-11-30[merlin] Adjust merlin for ide.Emilio Jesus Gallego Arias
2016-11-30Fix shelving order in typeclasses eauto.Théo Zimmermann
2016-11-30Fix typeclasses eauto shelving.Théo Zimmermann
2016-11-30Fix bug #5232: proper globalization of hints pathsMatthieu Sozeau
2016-11-30Univs: fix bug #5180Matthieu Sozeau
2016-11-30Fix #5183 - Two CoqIDE crash errorsMaxime Dénès
2016-11-30Update copyright on documentation cover.Maxime Dénès
2016-11-30Fix #5174: Underinformative syntax error messages in the new arguments syntaxMaxime Dénès
2016-11-29STM: cur_id must be invalid if an error occurs (fix #5191)Enrico Tassi
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-24Lazily load constants in micromega (bug #5134).Guillaume Melquiond
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-24Fix incorrect long multiplication in the VM.Guillaume Melquiond
2016-11-22Properly parenthesize "ltac:" arguments (bug #5169).Guillaume Melquiond
2016-11-21(v8.6) Update dev/doc/changes.txt with HintsResolveEntry changesJason Gross
2016-11-21(v8.6) Update dev/doc/changes with things about mem_named_contextJason Gross
2016-11-21(v8.6) Make a note about wit_constr and Constrarg in dev/doc/changesJason Gross
2016-11-21(v8.6) Add example in dev/doc/changes involving Tacmach.projectJason Gross
2016-11-21Remove spurious spaces in merlin file generated by coq_makefile (bug #5213).Guillaume Melquiond
2016-11-21Stop parsing -compat-notations options, which are no longer supported (bug #3...Guillaume Melquiond
2016-11-18Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Maxime Dénès
2016-11-18Revert "fake_ide: use the now available Status XML message"Maxime Dénès
2016-11-17Add missing label. Fixes broken ref.Théo Zimmermann
2016-11-17fake_ide: use the now available Status XML messageEnrico Tassi
2016-11-17Merge remote-tracking branch 'github/pr/360' into v8.6Maxime Dénès
2016-11-17Merge commit '633ed9c' into v8.6Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 04:26:55 +0000