aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-12-23Vi2vo: fix handling of univ constraints coming from the bodyEnrico Tassi
2014-12-23Minor modification of CHANGE.Pierre Courtieu
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Remove compatibility layer from Ltac's [fail].Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-21Dead code in Univ.Pierre-Marie Pédrot
2014-12-19Win32: fix installerEnrico Tassi
2014-12-19Install .v and .glob files tooEnrico Tassi
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
2014-12-19When pretyping [uconstr] closures, don't use the local Ltac variable environm...Arnaud Spiwack
2014-12-19Fixing performance issue of checker validation.Pierre-Marie Pédrot
2014-12-19Fixing checker representation of values.Pierre-Marie Pédrot
2014-12-19update md5 sums to make "make check" workEnrico Tassi
2014-12-19Fix sigsegv in checkerEnrico Tassi
2014-12-19Better doc and a few fixes for Proof using.Enrico Tassi
2014-12-19Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...Hugo Herbelin
2014-12-19Fixing wrong notation level in #3295.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 03:57:35 +0000