aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\
| * Fix anomaly when doing [all:Check _.] during a proof.Gravatar Gaetan Gilbert2017-04-14
* | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| * Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| * [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
|/
* Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* DocumentationGravatar Enrico Tassi2016-06-07
* STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06
* STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
* Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Gravatar Enrico Tassi2016-05-10
* Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Remove useless recursive flags.Gravatar Guillaume Melquiond2016-01-01
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
* | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Gravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
|/
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* STM: Reset takes Ltac <ident> into account (Close #4316)Gravatar Enrico Tassi2015-09-15
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* STM: if Set Universe Polymorphism then synchronous (#4119)Gravatar Enrico Tassi2015-03-22
* Reset "section name" works again (Close #3933)Gravatar Enrico Tassi2015-02-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* vernac_classifier: VernacDeclareTacticDefinition does not alter the parserGravatar Enrico Tassi2014-11-03
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* 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-11-26 09:51:31 +0000