aboutsummaryrefslogtreecommitdiff
path: root/stm/vernac_classifier.ml
AgeCommit message (Expand)Author
2016-11-18Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Maxime Dénès
2016-11-17[stm] Remove STM-related vernacularsEmilio Jesus Gallego Arias
2016-10-01Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Guillaume Melquiond
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-07DocumentationEnrico Tassi
2016-06-06STM: proof block detection for bullets and { block }Enrico Tassi
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-05-10Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"Enrico Tassi
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-01Remove useless recursive flags.Guillaume Melquiond
2015-12-18CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionMatej Kosik
2015-12-18CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Matej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
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-02-22 14:27:05 +0000