aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-12-27include test-suite/coqchk in the summary logEnrico Tassi
2014-12-27universes_of_constant: do a proper set union of body and type univsEnrico Tassi
2014-12-27Revert "Term: include a function to print terms"Enrico Tassi
2014-12-26new test for coqchkEnrico Tassi
2014-12-26coqchk: flush the pp buffer from time to timeEnrico Tassi
2014-12-26STM: do not call process_error twice (Close: 3880)Enrico Tassi
2014-12-26Call Evd.nf_constraints only on Univ Poly constantsEnrico Tassi
2014-12-26STM: remove dead codeEnrico Tassi
2014-12-26Term: include a function to print termsEnrico Tassi
2014-12-25Document 6d5b56d971 (forbid Require inside modules).Maxime Dénès
2014-12-25Forbid Require inside interactive modules and module types.Maxime Dénès
2014-12-25Inlining Spawn.kill_if in the one place were it was actually used, thusPierre-Marie Pédrot
2014-12-23STM: cleanup code for AdmittedEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:06:40 +0000