aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-01-08Fixing compilation of penultimate commit d08532d.Hugo Herbelin
2015-01-08Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ...Hugo Herbelin
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2015-01-08Update + English in CHANGESHugo Herbelin
2015-01-08Start credits for 8.5.Matthieu Sozeau
2015-01-08Small fix in whodidwhat 8.5.Pierre Courtieu
2015-01-08Fixed and extend bullet related info/error messages. + doc.Pierre Courtieu
2015-01-08Fix some documentation typos.Guillaume Melquiond
2015-01-08Add a few words in whodidwhat.Maxime Dénès
2015-01-08Document native_compute.Maxime Dénès
2015-01-07Initiating who-did-what for 8.5Hugo Herbelin
2015-01-07Committing whodidwhat files.Hugo Herbelin
2015-01-07Reverting the tentative try to restore the use of second-orderHugo Herbelin
2015-01-07Aligning printing of universe constraints.Hugo Herbelin
2015-01-07Hook when state arrives on master.Enrico Tassi
2015-01-06Fix checker's treatment of template polymorphicMatthieu Sozeau
2015-01-06Safer version of the implementation of stores.Pierre-Marie Pédrot
2015-01-06remove unused iArrayEnrico Tassi
2015-01-06rename: vi -> vioEnrico Tassi
2015-01-06Fix some documentation typos.Guillaume Melquiond
2015-01-06Fix setoid rewrite.Arnaud Spiwack
2015-01-06Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug #38...Guillaume Melquiond
2015-01-06updated include file for debuggingBruno Barras
2015-01-06improve efficiency of the reduction interpreter of coqtopBruno Barras
2015-01-06improve efficiency of the reduction interpreter of the checkerBruno Barras
2015-01-06Fixing test for bug #2830.Pierre-Marie Pédrot
2015-01-06Rename ill-named "imports" field of safe_env into "required".Maxime Dénès
2015-01-06Propagating the relaxing of filtering started in 48509b6, fixed inHugo Herbelin
2015-01-06Fixing old filter bug in second_order_matching.Hugo Herbelin
2015-01-05Added more informative messages about bullets.Pierre Courtieu
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2015-01-05In Show Universes, print universes before normalization.Matthieu Sozeau
2015-01-05Updating documentation about bullets.Pierre Courtieu
2015-01-05Removing GUtil dependency from ide/document.ml.Pierre-Marie Pédrot
2015-01-05Adding an option to deactivate the progress bar.Pierre-Marie Pédrot
2015-01-05Implementing a segment-viewer in CoqIDE.Pierre-Marie Pédrot
2015-01-04STM: Make assert unneeded (Close 3898)Enrico Tassi
2015-01-04Adapting two files from test-suite to now forbidden Require's in modules.Hugo Herbelin
2015-01-03Fixing 48509b61 which improved unification as expected but actuallyHugo Herbelin
2015-01-03Fixing #3896 (incorrect sigma given to printer).Hugo Herbelin
2015-01-03Tentatively trying to restore the use of second-order typed-basedHugo Herbelin
2015-01-03Fixing #3895 (thanks to PMP for diagnosis).Hugo Herbelin
2015-01-01An optimization in the use of unification candidates so as to get theHugo Herbelin
2014-12-30Document the new behavior of lazymatch.Guillaume Melquiond
2014-12-30Fixing #3892: Ensure that notation variables do not capture namesHugo Herbelin
2014-12-30Simplifying second_order_matching: no need to invert the linearHugo Herbelin
2014-12-30Compatibility ocaml 3.12.Hugo Herbelin
2014-12-30more CHANGESEnrico Tassi
2014-12-30Minor fixes for the win32 installerEnrico Tassi
2014-12-29Fixing bug #3632 for good.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:12:24 +0000