aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-30CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleanedPierre Letouzey
2014-01-30Mltop: explicitly qualify calls to CUnixPierre Letouzey
2014-01-30Load implemented in CoqIDE/STM (closes: #3223)Enrico Tassi
2014-01-30STM + CoqIDE: stop_worker message and UIEnrico Tassi
2014-01-30Work around for bug in threads + blocking io streamlinedEnrico Tassi
2014-01-30STM: worker sends back to master the last valid stateEnrico Tassi
2014-01-30STM: tell the user if the master is recomputing states validated by workersEnrico Tassi
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2014-01-26-schedule-vi-checking ported to spawnEnrico Tassi
2014-01-26break > 80 cols lineEnrico Tassi
2014-01-26STM: ported to spawnEnrico Tassi
2014-01-26CoqIDE: ported to spawnEnrico Tassi
2014-01-14-schedule-vi-checking generates better scriptEnrico Tassi
2014-01-14STM: fix -async-proofs lazyEnrico Tassi
2014-01-13Make Require verbosePierre Boutillier
2014-01-13STM: fix very simple demoEnrico Tassi
2014-01-13Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Pierre Boutillier
2014-01-07typosEnrico Tassi
2014-01-06STM: handle side effects of workers correctlyEnrico Tassi
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2014-01-05STM: modules do not prevent proofs from being ASyncEnrico Tassi
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2014-01-05Fix coqc -time (Closes: 3201)Enrico Tassi
2014-01-05STM: fix error messages while in batch mode (closes: 3196)Enrico Tassi
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2014-01-05Fix some warnings with ocamlc 4.01Enrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04Lemmas: export standard proof terminatorEnrico Tassi
2014-01-04Proof_global: Simpler API for proof_terminatorEnrico Tassi
2014-01-04STM: use sec vars in aux file if no Proof using when building .viEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2014-01-04STM: simple refactoringEnrico Tassi
2014-01-04STM: set loc for aux file when interpreting vernacEnrico Tassi
2014-01-04STM: record in aux file proof build and check timeEnrico Tassi
2013-12-30Useless Evd.create_evar_defs.Pierre-Marie Pédrot
2013-12-24STM: capture type checking error (Closes: 3195)Enrico Tassi
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-24CoqIDE: new feedback "incomplete" to signal partial QedEnrico Tassi
2013-12-24cleanup warningEnrico Tassi
2013-12-22Adding a finer-grained -bt flag to coqtop only triggering backtraces.Pierre-Marie Pédrot
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-Marie Pédrot
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
2013-12-10Fix CoqIDE on windowsEnrico Tassi
2013-12-09Fix printing of Ltac's backtrace.Arnaud Spiwack
2013-12-04Stm: remove an assertion.Arnaud Spiwack
2013-12-04Fix Admitted.Arnaud Spiwack
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 08:46:16 +0000