aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* STM: fix Show ScriptGravatar Enrico Tassi2014-03-04
* STM: when finish a task hcons universe constraintsGravatar Enrico Tassi2014-03-04
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Migrate back g_obligations in toplevelGravatar Pierre Letouzey2014-03-02
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
* Removing a fishy use of pervasive equality in Ltac backtrace printing.Gravatar Pierre-Marie Pédrot2014-03-01
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
* STM: better debug messagesGravatar Enrico Tassi2014-02-26
* STM: do not print goals on UndoGravatar Enrico Tassi2014-02-26
* CoqIDE: print message of "Fail" commandGravatar Enrico Tassi2014-02-26
* STM: better messages when checking/finishing tasksGravatar Enrico Tassi2014-02-26
* vi2vo: new flag -schedule-vi2voGravatar Enrico Tassi2014-02-26
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* STM: backup/restore remote countersGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Fixing printing of only_parsing notations.Gravatar Pierre-Marie Pédrot2014-02-25
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* Dead Code eliminationGravatar Pierre Boutillier2014-02-24
* Timeout and Set Default Timeout fixed (closes: #3229)Gravatar Enrico Tassi2014-02-10
* STM: when a worker is canceled mark the proof as brokenGravatar Enrico Tassi2014-02-10
* STM: be conservative w.r.t. proofs containing global side effectsGravatar Enrico Tassi2014-02-10
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 23:15:11 +0000