aboutsummaryrefslogtreecommitdiff
path: root/intf/vernacexpr.mli
AgeCommit message (Expand)Author
2016-06-20COMMENTS: Vernacexpr.extend_nameMatej Kosik
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-16Extend Hint Mode to handle the no-head-evar caseMatthieu Sozeau
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-16Merge remote-tracking branch 'github/pr/194' into trunkMaxime Dénès
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
2016-06-07Adding an only printing flag to notations.Pierre-Marie Pédrot
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Print Ltac 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-03-06Moving Autorewrite to Hightatctic.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-11CLEANUP: removing unnecessary wrapperMatej Kosik
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2015-12-18CLEANUP: removing unnecessary aliasMatej Kosik
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-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-10-08Proof using: let-in policy, optional auto-clear, forward closure*Enrico Tassi
2015-10-08Goptions: new value type: optional stringEnrico Tassi
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-08-19Documentation by giving a name to a large type.Pierre-Marie Pédrot
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-06-29Code documentation of the TACTIC/VERNAC EXTEND macros.Pierre-Marie Pédrot
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-15About now accepts hypothesis names and goal selector.Pierre Courtieu
2014-12-12Searchxxx now search also the hypothesis and support goal selector.Pierre Courtieu
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-13Emit a warning for void Arguments statement (Close 3713)Enrico Tassi
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-12Add syntax [id]: to apply tactic to goal named id.Hugo Herbelin
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-09-04Add a [Variant] declaration which allows to write non-recursive variant types.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 17:36:36 +0000