aboutsummaryrefslogtreecommitdiff
path: root/intf/vernacexpr.mli
AgeCommit message (Expand)Author
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-24[location] Use located in misctypes.Emilio Jesus Gallego Arias
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-09Removing internal support for accepting "{struct x}" and co in "Theorem with".Hugo Herbelin
2017-04-03Merge PR#417: No cast surgery in let inMaxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
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-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-01Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Guillaume Melquiond
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
2016-09-29Fix bug #4798: compat notations should not modify the parser.Pierre-Marie Pédrot
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-08Making Vernacexpr independent from Tacexpr.Pierre-Marie Pédrot
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:46:42 +0000