aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.mli
Commit message (Expand)AuthorAge
* Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
* Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\
* | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| * Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\
| * 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
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\ \
| | * Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
| |/
| * Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
| |\
| * | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
| * | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| | * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| |/
* / Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
|/
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* COMMENTS: Vernacexpr.extend_nameGravatar Matej Kosik2016-06-20
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
* Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\
* \ Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \
| | * Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| | * Add goal range selectors.Gravatar Cyprien Mangin2016-06-14
| * | Adding an only printing flag to notations.Gravatar Pierre-Marie Pédrot2016-06-07
| |/
* / STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
|/
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\
* | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Print Ltac 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
* | Moving Autorewrite to Hightatctic.Gravatar Pierre-Marie Pédrot2016-03-06
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
* | | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | | CLEANUP: removing unnecessary aliasGravatar Matej Kosik2015-12-18
* | | 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
|/ /
* | Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* | Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* | Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* | Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
* | Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* | Documentation by giving a name to a large type.Gravatar Pierre-Marie Pédrot2015-08-19
| * Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Gravatar Jason Gross2015-08-14
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 03:12:17 +0000