aboutsummaryrefslogtreecommitdiff
path: root/intf
AgeCommit message (Expand)Author
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-12-18CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedMatej Kosik
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-18COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of "Glob_term.glob_constr" type.Matej Kosik
2015-12-18COMMENTS: added to some variants of the "Constrexpr.prim_token" type.Matej Kosik
2015-12-18CLEANUP: Vernacexpr.vernac_exprMatej Kosik
2015-12-04Getting rid of the dynamic node of the tactic AST.Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Dead code from August 2014 in apply in.Hugo Herbelin
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-28Fixing the return type of the Atoken symbol.Pierre-Marie Pédrot
2015-10-27Type-safe grammar extensions.Pierre-Marie Pédrot
2015-10-19Type delayed_open_constr is now monotonic.Pierre-Marie Pédrot
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
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-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-08-22Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-19Documentation by giving a name to a large type.Pierre-Marie Pédrot
2015-07-02Merge branch 'v8.5' into trunkMaxime Dénès
2015-06-29Code documentation of the TACTIC/VERNAC EXTEND macros.Pierre-Marie Pédrot
2015-06-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-06-25Remove other types not carried by interpretations in `Tacexpr`.Arnaud Spiwack
2015-06-25Remove useless `and_short_name` in interpreted level in `Tacexpr`.Arnaud Spiwack
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-23A global [gfail] tactic which works like [fail] except that it fails even if ...Arnaud Spiwack
2014-12-23Fix compilation error in some configurations.Arnaud Spiwack
2014-12-19Add a backtracking version of Ltac's [match].Arnaud Spiwack
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-12Add Ltac syntax for the [tclIFCATCH] primitive.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 22:15:47 +0000