| Age | Commit message (Expand) | Author |
|---|---|---|
| 2017-10-01 | Using Ltac2 native closures in some tactic APIs. | Pierre-Marie Pédrot |
| 2017-10-01 | Rolling up our own representation of clauses. | Pierre-Marie Pédrot |
| 2017-10-01 | Moving ML types used by Ltac2 to their proper interface. | Pierre-Marie Pédrot |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |