aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-12-29Proof using: do not clear letins (unless they use a cleared var)Enrico Tassi
2014-12-28Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...Arnaud Spiwack
2014-12-28Call nf_constraints also when compiling directly to voEnrico Tassi
2014-12-28Proof using: call "clear" to remove from sight the vars not selectedEnrico Tassi
2014-12-28remove debug prints (leftover)Enrico Tassi
2014-12-27STM: check with the kernel proof terms on the worker tooEnrico Tassi
2014-12-27STM: fix processing of errorsEnrico Tassi
2014-12-27STM: module Pp is openEnrico Tassi
2014-12-27proof_global: make it possible to call close_proof in a workerEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:25:22 +0000