| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-10-29 | Fix #10615: Notation substitution for Ltac2 terms. | Pierre-Marie Pédrot | |
| We implement a new type of "preterms" that represent untyped ASTs, corresponding to glob_expr in the ML implementations. Ltac2 quotations inside notations are provided with such preterms, and have to pretype them in order to do anything of relevance with them. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |