aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Expand)AuthorAge
* Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* 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
* COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.Gravatar Matej Kosik2015-12-18
* COMMENTS: added to some variants of "Glob_term.glob_constr" type.Gravatar Matej Kosik2015-12-18
* COMMENTS: added to some variants of the "Constrexpr.prim_token" type.Gravatar Matej Kosik2015-12-18
* CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
* Getting rid of the dynamic node of the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\
| * Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* | Fixing the return type of the Atoken symbol.Gravatar Pierre-Marie Pédrot2015-10-28
* | Type-safe grammar extensions.Gravatar Pierre-Marie Pédrot2015-10-27
* | Type delayed_open_constr is now monotonic.Gravatar Pierre-Marie Pédrot2015-10-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-12
|\|
| * Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * 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 Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|\|
| * Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-22
|\|
| * Documentation by giving a name to a large type.Gravatar Pierre-Marie Pédrot2015-08-19
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
|\|
| * Code documentation of the TACTIC/VERNAC EXTEND macros.Gravatar Pierre-Marie Pédrot2015-06-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-28
|\|
| * Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* | Remove other types not carried by interpretations in `Tacexpr`.Gravatar Arnaud Spiwack2015-06-25
* | Remove useless `and_short_name` in interpreted level in `Tacexpr`.Gravatar Arnaud Spiwack2015-06-25
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* | Merge branch 'v8.5' into trunkGravatar Enrico Tassi2015-03-30
|\|
| * Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-15
|\|
| * Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-10
|\|
| * Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* | Embedding the index of the ML tactic entry in the Tacexpr AST.Gravatar Pierre-Marie Pédrot2015-01-21
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19