aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Expand)AuthorAge
* Removing the UConstr entry of the tactic_arg AST.Gravatar Pierre-Marie Pédrot2016-03-04
* Moving the "move" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "exists" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "symmetry" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "generalize dependent" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "clearbody" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "clear" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "cofix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "fix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Printing notations: Cleaning in anticipation of fixing #4592.Gravatar Hugo Herbelin2016-02-28
* Removing the MetaIdArg entry of tactic expressions.Gravatar Pierre-Marie Pédrot2016-02-24
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* | New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Gravatar Hugo Herbelin2016-01-21
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Separating the parsing of user-defined entries from their intepretation.Gravatar Pierre-Marie Pédrot2016-01-16
* | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
* | COMMENTS: added to the "Constrexpr.CCases" variant.Gravatar Matej Kosik2016-01-11
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 08:36:07 +0000