| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-26 | Do not expand trivial patterns in functions. | Pierre-Marie Pédrot | |
| 2017-07-26 | Ensuring that inductive constructors are always capitalized. | Pierre-Marie Pédrot | |
| 2017-07-26 | Adding a file for testing typing. | Pierre-Marie Pédrot | |
| 2017-07-26 | Fix typo in error message | Pierre-Marie Pédrot | |
| 2017-07-26 | Better typing errors for function types. | Pierre-Marie Pédrot | |
| 2017-07-26 | Lightweight quotation syntax for terms and idents. | Pierre-Marie Pédrot | |
| 2017-07-26 | Properly handling toplevel recursive definitions. | Pierre-Marie Pédrot | |
| 2017-07-26 | Exporting some basic tactics from Ltac1. | Pierre-Marie Pédrot | |
| 2017-07-26 | Bugfix: wrong access to non-constant constructor compilation. | Pierre-Marie Pédrot | |
| 2017-07-25 | Generalizing patterns in fun bindings. | Pierre-Marie Pédrot | |
| 2017-07-24 | Adding a few primitive functions. | Pierre-Marie Pédrot | |
| 2017-07-24 | Correctly pushing variables for tuple patterns. | Pierre-Marie Pédrot | |
| 2017-07-24 | Properly handle parsing of list patterns. | Pierre-Marie Pédrot | |
| 2017-07-24 | Fix typo. | Pierre-Marie Pédrot | |
| 2017-07-24 | Removing a spurious file. | Pierre-Marie Pédrot | |
| 2017-07-24 | Filling the README. | Pierre-Marie Pédrot | |
| 2017-07-24 | Adding quick-n-dirty tests. | Pierre-Marie Pédrot | |
| 2017-07-24 | Fix library hardwired prefix. | Pierre-Marie Pédrot | |
| 2017-07-24 | Turning the ltac2 subfolder into a standalone plugin. | Pierre-Marie Pédrot | |
| 2017-05-19 | Adding new tactic notation scopes. | Pierre-Marie Pédrot | |
| 2017-05-19 | Extending the Coq API in Ltac2. | Pierre-Marie Pédrot | |
| 2017-05-19 | Removing dead code in Ltac2, and cleaning up a bit. | Pierre-Marie Pédrot | |
| 2017-05-19 | Introducing tactic notations in Ltac2. | Pierre-Marie Pédrot | |
| 2017-05-19 | Allow raw terms to contain references to absolute definitions. | Pierre-Marie Pédrot | |
| 2017-05-19 | Stdlib functions now return Ltac2 exceptions. | Pierre-Marie Pédrot | |
| 2017-05-19 | Proper handling of exception definition in Ltac2. | Pierre-Marie Pédrot | |
| We actually implemented a full-fledged open type system, so that exceptions are a special case of it. | |||
| 2017-05-19 | Merging GTacTuple and GTacCst nodes. | Pierre-Marie Pédrot | |
| 2017-05-19 | Towards a proper printing of Ltac2 data structures. | Pierre-Marie Pédrot | |
| 2017-05-19 | Allow the embedding of Ltac2 terms in constrs via the ltac2:(...) syntax. | Pierre-Marie Pédrot | |
| 2017-05-19 | Fixing a precedence issue in type parameters. | Pierre-Marie Pédrot | |
| 2017-05-19 | Proper handling of record types. | Pierre-Marie Pédrot | |
| We add the standard ML facilities for records, that is, projections, mutable fields and primitive to set them. | |||
| 2017-05-19 | Allowing to include Coq terms in Ltac2 using the constr:(...) syntax. | Pierre-Marie Pédrot | |
| 2017-05-19 | Embedding generic arguments in Ltac2 AST. | Pierre-Marie Pédrot | |
| 2017-05-19 | Introduction of the Ltac2 plugin. | Pierre-Marie Pédrot | |
| For now, it is only a simple mini-ML whose effects are the proofview monad. There is no facility to manipulate terms nor any hardwired tactic. Pattern-matching is restricted to superficial constructors, the language is lacking a lot of user-friendly interfaces, the grammar is crappy, and much more. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |