aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.ml
Commit message (Expand)AuthorAge
...
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Gravatar Enrico Tassi2014-09-09
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* STM: Classify Let as non asynchronous (Closes: #3486)Gravatar Enrico Tassi2014-08-05
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Gravatar Arnaud Spiwack2014-06-06
* 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
* 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
* 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
* 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-27 00:06:54 +0000