aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleanedGravatar Pierre Letouzey2014-01-30
* Mltop: explicitly qualify calls to CUnixGravatar Pierre Letouzey2014-01-30
* Load implemented in CoqIDE/STM (closes: #3223)Gravatar Enrico Tassi2014-01-30
* STM + CoqIDE: stop_worker message and UIGravatar Enrico Tassi2014-01-30
* Work around for bug in threads + blocking io streamlinedGravatar Enrico Tassi2014-01-30
* STM: worker sends back to master the last valid stateGravatar Enrico Tassi2014-01-30
* STM: tell the user if the master is recomputing states validated by workersGravatar Enrico Tassi2014-01-30
* Fixing backtrace handling here and there.Gravatar Pierre-Marie Pédrot2014-01-30
* -schedule-vi-checking ported to spawnGravatar Enrico Tassi2014-01-26
* break > 80 cols lineGravatar Enrico Tassi2014-01-26
* STM: ported to spawnGravatar Enrico Tassi2014-01-26
* CoqIDE: ported to spawnGravatar Enrico Tassi2014-01-26
* -schedule-vi-checking generates better scriptGravatar Enrico Tassi2014-01-14
* STM: fix -async-proofs lazyGravatar Enrico Tassi2014-01-14
* Make Require verboseGravatar Pierre Boutillier2014-01-13
* STM: fix very simple demoGravatar Enrico Tassi2014-01-13
* Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Gravatar Pierre Boutillier2014-01-13
* typosGravatar Enrico Tassi2014-01-07
* STM: handle side effects of workers correctlyGravatar Enrico Tassi2014-01-06
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
* STM: modules do not prevent proofs from being ASyncGravatar Enrico Tassi2014-01-05
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Fix coqc -time (Closes: 3201)Gravatar Enrico Tassi2014-01-05
* STM: fix error messages while in batch mode (closes: 3196)Gravatar Enrico Tassi2014-01-05
* Paral-ITP: cleanup of command line flags and more conservative defaultGravatar Enrico Tassi2014-01-05
* Fix some warnings with ocamlc 4.01Gravatar Enrico Tassi2014-01-05
* coqtop: -check-vi-tasks and -schedule-vi-checkingGravatar Enrico Tassi2014-01-05
* Lemmas: export standard proof terminatorGravatar Enrico Tassi2014-01-04
* Proof_global: Simpler API for proof_terminatorGravatar Enrico Tassi2014-01-04
* STM: use sec vars in aux file if no Proof using when building .viGravatar Enrico Tassi2014-01-04
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* STM: simple refactoringGravatar Enrico Tassi2014-01-04
* STM: set loc for aux file when interpreting vernacGravatar Enrico Tassi2014-01-04
* STM: record in aux file proof build and check timeGravatar Enrico Tassi2014-01-04
* Useless Evd.create_evar_defs.Gravatar Pierre-Marie Pédrot2013-12-30
* STM: capture type checking error (Closes: 3195)Gravatar Enrico Tassi2013-12-24
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* CoqIDE: new feedback "incomplete" to signal partial QedGravatar Enrico Tassi2013-12-24
* cleanup warningGravatar Enrico Tassi2013-12-24
* Adding a finer-grained -bt flag to coqtop only triggering backtraces.Gravatar Pierre-Marie Pédrot2013-12-22
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* A few fixes to the build system (mostly for ocamlbuild)Gravatar Pierre Letouzey2013-12-16
* Fix CoqIDE on windowsGravatar Enrico Tassi2013-12-10
* Fix printing of Ltac's backtrace.Gravatar Arnaud Spiwack2013-12-09
* Stm: remove an assertion.Gravatar Arnaud Spiwack2013-12-04
* Fix Admitted.Gravatar Arnaud Spiwack2013-12-04
* Factoring(continued).Gravatar Arnaud Spiwack2013-12-04
* Refactoring: storing more information in the terminator closure.Gravatar Arnaud Spiwack2013-12-04
* The commands that initiate proofs are now in charge of what happens when proo...Gravatar Arnaud Spiwack2013-12-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 17:29:27 +0000