aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-01Allowing the "Declare Instance" command anywhere. This was artificiallyPierre-Marie Pédrot
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
2014-04-25Removing Autoinstance once and for all.Pierre-Marie Pédrot
2014-04-25Removing useless try-with clauses in Goal.enter variants.Pierre-Marie Pédrot
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 14:58:42 +0000