aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-04-09Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...Pierre Boutillier
2014-04-08Add an option -Q (tentative name).Guillaume Melquiond
2014-04-07Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...Guillaume Melquiond
2014-04-06Change handling of loadpath and mlpath.Guillaume Melquiond
2014-04-02STM: be more resilient to explicit Back + Sideff commands (closes: 3251)Enrico Tassi
2014-03-31Removing dead code in Tactics.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-26STM: when an error occurs in a worker send back a bunch of statesEnrico Tassi
2014-03-19Adding a Print Strategy vernacular command. It allows to check thePierre-Marie Pédrot
2014-03-18STM: make the slave start from the most recent known stateEnrico Tassi
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-13fix compilation with ocaml < 4Enrico Tassi
2014-03-13STM: perspective (tell the scheduler what the user sees)Enrico Tassi
2014-03-13STM: move out a couple of submodulesEnrico Tassi
2014-03-12Stm: smarter delegation policyEnrico Tassi
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-06Lets coqtop use a slashVirgile Prevosto
2014-03-05Using HMaps in Safe_env.environments, hopefully improving performances.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-04STM: fix Show ScriptEnrico Tassi
2014-03-04STM: when finish a task hcons universe constraintsEnrico Tassi
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2014-03-02Migrate back g_obligations in toplevelPierre Letouzey
2014-03-01Useless check when loading notations through import.Pierre-Marie Pédrot
2014-03-01Removing a fishy use of pervasive equality in Ltac backtrace printing.Pierre-Marie Pédrot
2014-02-27Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Arnaud Spiwack
2014-02-26STM: better debug messagesEnrico Tassi
2014-02-26STM: do not print goals on UndoEnrico Tassi
2014-02-26CoqIDE: print message of "Fail" commandEnrico Tassi
2014-02-26STM: better messages when checking/finishing tasksEnrico Tassi
2014-02-26vi2vo: new flag -schedule-vi2voEnrico Tassi
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26STM: backup/restore remote countersEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-25Fixing printing of only_parsing notations.Pierre-Marie Pédrot
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2014-02-24Dead Code eliminationPierre Boutillier
2014-02-10Timeout and Set Default Timeout fixed (closes: #3229)Enrico Tassi
2014-02-10STM: when a worker is canceled mark the proof as brokenEnrico Tassi
2014-02-10STM: be conservative w.r.t. proofs containing global side effectsEnrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 17:57:47 +0000