aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Fix context forgetting universes (temporary, the fix is not exactly right).Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* - Fix handling of polymorphic inductive elimination schemes.Gravatar Matthieu Sozeau2014-05-06
* Various fixes of universe polymorphism and projections when they're set.Gravatar Matthieu Sozeau2014-05-06
* - Fix Check to use the constraints inferred during type inference.Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 11:52:41 +0000