aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-11-08Use pf_get_type_of to avoid blowup in pose proof of large proof termsMatthieu Sozeau
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-11-07Improve formatting of a message in [Arguments].Maxime Dénès
2016-11-07Fix #5181: [Arguments] no longer correctly checks the length of arguments listsMaxime Dénès
2016-11-07Fix #5182: "Arguments names must be distinct." is bogus and underinformativeMaxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-05Not using style tags when translating/beautifying a file.Hugo Herbelin
2016-11-05Removing a special treatment for empty lines in comments.Hugo Herbelin
2016-11-05Removing obsolete parsing of strings à la v7 in comments.Hugo Herbelin
2016-11-05Do not print dependent evars by default (expensive)Matthieu Sozeau
2016-11-05More precise refine compatibilityMatthieu Sozeau
2016-11-04Quick fix of tactic parsing while Load-ing in coqide.Hugo Herbelin
2016-11-04Test for #4966 ("auto" wrongly seen as "auto with *" when in position of ident).Hugo Herbelin
2016-11-04Fix #3441 Use pf_get_type_of to avoid blowupMatthieu Sozeau
2016-11-04Fix refine in compatibility modeMatthieu Sozeau
2016-11-04Fix #4837: ./configure -local makes coqdep issue many warningsMaxime Dénès
2016-11-04Merge remote-tracking branch 'github/pr/335' into v8.6Maxime Dénès
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-11-04Add documentation for [Set Warnings] and the -w option.Cyprien Mangin
2016-11-04Silence option deprecation warnings in the compat fileJason Gross
2016-11-03Remove an OCaml 4.02 construct.Maxime Dénès
2016-11-03Merge remote-tracking branch 'github/pr/340' into v8.6Maxime Dénès
2016-11-03Merge remote-tracking branch 'github/pr/341' into v8.6Maxime Dénès
2016-11-02Better Arguments compatibility.Maxime Dénès
2016-11-02Fix various shortcomings of the warnings infrastructure.Maxime Dénès
2016-11-02Put string between quotes when printing an option value.Maxime Dénès
2016-10-30Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-29Removing dead code.Hugo Herbelin
2016-10-29Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).Hugo Herbelin
2016-10-29Fixing #5164 (regression in locating error in argument of "refine").Hugo Herbelin
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
2016-10-28Merge commit 'fccbd64' into v8.6Maxime Dénès
2016-10-28[build] Add a target to install the META file.Emilio Jesus Gallego Arias
2016-10-28[build] META file to enable plugin linking with ocamlfind.Emilio Jesus Gallego Arias
2016-10-28Merge remote-tracking branch 'github/pr/337' into v8.6Maxime Dénès
2016-10-27Fixing #5161 (case of a notation with unability to detect a recursive binder).Hugo Herbelin
2016-10-27Add missing dot to impargs error message.Maxime Dénès
2016-10-27Proper fix for #3753 (anomaly with implicit arguments and renamings)Maxime Dénès
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-26Using msg_info for info_auto and info_eauto (PR #324).Hugo Herbelin
2016-10-26STM: make ~valid state id non optional from APIsEnrico Tassi
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-25Merge remote-tracking branch 'github/pr/338' into v8.5Maxime Dénès
2016-10-25Remove warning now that info_auto is fixed.Théo Zimmermann
2016-10-25Remove v62 from the refman.Théo Zimmermann
2016-10-25Remove v62 from the codebase.Théo Zimmermann
2016-10-25Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Maxime Dénès
2016-10-25Merge commit 'a799600' into v8.6Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 11:14:58 +0000