aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-12-18Adds two lemmas about hderror to the List standard library.Sébastien Hinderer
2014-12-18Implement the nodup function on lists and prove associated results.Sébastien Hinderer
2014-12-18Lists: enhanced version of Seb's last commit on Exists/ForallPierre Letouzey
2014-12-18Lists: a few results on Exists and Forall and a bit of code cleanup.Sébastien Hinderer
2014-12-18Fixing checker representation of universe lists.Pierre-Marie Pédrot
2014-12-18Backporting the change in lists of universes to the checker.Pierre-Marie Pédrot
2014-12-18Cleaning up universe list implementation in Univ.Pierre-Marie Pédrot
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-18Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for gram...mlasson
2014-12-18Fixed bad newlines in output for std output and emacs.Pierre Courtieu
2014-12-17Fix compilation with ocaml 4.0.0Enrico Tassi
2014-12-17checker: Change in library on disk values, now using context_sets instead ofMatthieu Sozeau
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-12-17Fix (actually, properly implement :) hashconsing of projections,Matthieu Sozeau
2014-12-17Fixing bug #3796.Pierre-Marie Pédrot
2014-12-17Fixing Makefile so that it puts the -thread flag on the right place.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 14:54:06 +0000