aboutsummaryrefslogtreecommitdiff
path: root/intf
AgeCommit message (Expand)Author
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-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
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
2014-12-12Extend the syntax of simpl with a delta flag.Arnaud Spiwack
2014-12-12Searchxxx now search also the hypothesis and support goal selector.Pierre Courtieu
2014-12-11Tentatively more informative report of failure when inferringHugo Herbelin
2014-12-07Improved tracking of the origin of evars.Hugo Herbelin
2014-11-16Enforcing a stronger difference between the two syntaxes "simplHugo Herbelin
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-01Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.Arnaud Spiwack
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-13Emit a warning for void Arguments statement (Close 3713)Enrico Tassi
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 23:24:53 +0000