aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* Fixing universe substitution in mutual fixpoints.Gravatar Pierre-Marie Pédrot2014-07-16
* STM: check-vi-task fixedGravatar Enrico Tassi2014-07-16
* STM: Goal printing got wrong in a merge, fixedGravatar Enrico Tassi2014-07-16
* STM: let toploop plugins specify the flags for STM workersGravatar Enrico Tassi2014-07-11
* STM: flag to turn off branch reopeningGravatar Enrico Tassi2014-07-11
* STM: add optionally takes the id of the new tipGravatar Enrico Tassi2014-07-11
* STM: export the observe function (useful for pide)Gravatar Enrico Tassi2014-07-11
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
* option to always delegate futures to workersGravatar Enrico Tassi2014-07-10
* more APIs in TQueue and CThreadGravatar Enrico Tassi2014-07-10
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Patch from Enrico Tassi to get Drop compatible with stm.Gravatar Enrico Tassi2014-07-01
* Typo in stm error message.Gravatar Hugo Herbelin2014-06-28
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* cut toploop(s) out of coqtop: now they are loaded dynamicallyGravatar Enrico Tassi2014-06-25
* Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Gravatar Enrico Tassi2014-06-23
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* STM: handle "Time Abort" correctly (Closes: 3332)Gravatar Enrico Tassi2014-06-08
* Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Gravatar Arnaud Spiwack2014-06-06
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
* Polymorphic Lemmas are like Defined ones for STMGravatar Enrico Tassi2014-05-15
* - 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
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* Cleanup in constr, correct classification of polymorphic defs.Gravatar Matthieu Sozeau2014-05-06
* Lemmas: export standard proof terminatorGravatar Enrico Tassi2014-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
* Fixing ml-doc.Gravatar 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 19:22:01 +0000