aboutsummaryrefslogtreecommitdiff
path: root/stm/vernac_classifier.ml
AgeCommit message (Expand)Author
2015-09-15STM: Reset takes Ltac <ident> into account (Close #4316)Enrico Tassi
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-03-22STM: if Set Universe Polymorphism then synchronous (#4119)Enrico Tassi
2015-02-15Reset "section name" works again (Close #3933)Enrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-03vernac_classifier: VernacDeclareTacticDefinition does not alter the parserEnrico Tassi
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-09-10VernacExtend does not dispatch on type anymore.Pierre-Marie Pédrot
2014-09-09Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)Enrico Tassi
2014-09-04Remove [Infer] option of records.Arnaud Spiwack
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-05STM: Classify Let as non asynchronous (Closes: #3486)Enrico Tassi
2014-08-04STM: VtQuery holds the id of the state it refers toCarst Tankink
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-06Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Arnaud Spiwack
2014-05-15poly: remove unused attribute to STM nodes and vernac classificaitonEnrico Tassi
2014-05-15Polymorphic Lemmas are like Defined ones for STMEnrico Tassi
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06Cleanup in constr, correct classification of polymorphic defs.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-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:05:51 +0000