aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Allowing the "Declare Instance" command anywhere. This was artificiallyGravatar Pierre-Marie Pédrot2014-05-01
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
* Removing Autoinstance once and for all.Gravatar Pierre-Marie Pédrot2014-04-25
* Removing useless try-with clauses in Goal.enter variants.Gravatar Pierre-Marie Pédrot2014-04-25
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Have the feedback bus as a backend for dumping globs.Gravatar Carst Tankink2014-04-10
* Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...Gravatar Pierre Boutillier2014-04-09
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
* Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...Gravatar Guillaume Melquiond2014-04-07
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
* STM: be more resilient to explicit Back + Sideff commands (closes: 3251)Gravatar Enrico Tassi2014-04-02
* Removing dead code in Tactics.Gravatar Pierre-Marie Pédrot2014-03-31
* Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Gravatar Pierre-Marie Pédrot2014-03-26
* STM: when an error occurs in a worker send back a bunch of statesGravatar Enrico Tassi2014-03-26
* Adding a Print Strategy vernacular command. It allows to check theGravatar Pierre-Marie Pédrot2014-03-19
* STM: make the slave start from the most recent known stateGravatar Enrico Tassi2014-03-18
* STM: make -async-proofs on work from coqc tooGravatar Enrico Tassi2014-03-18
* fix compilation with ocaml < 4Gravatar Enrico Tassi2014-03-13
* STM: perspective (tell the scheduler what the user sees)Gravatar Enrico Tassi2014-03-13
* STM: move out a couple of submodulesGravatar Enrico Tassi2014-03-13
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Using Hashmaps by default in constant and inductive maps. This changes fold andGravatar Pierre-Marie Pédrot2014-03-07
* Lets coqtop use a slashGravatar Virgile Prevosto2014-03-06
* Using HMaps in Safe_env.environments, hopefully improving performances.Gravatar Pierre-Marie Pédrot2014-03-05
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 22:52:33 +0000