| Age | Commit message (Expand) | Author |
|---|---|---|
| 2017-09-14 | Moving valexpr definition to Tac2ffi. | Pierre-Marie Pédrot |
| 2017-09-08 | Fix coq/ltac2#22: Argument to Tactic_failure should be printed. | Pierre-Marie Pédrot |
| 2017-09-02 | Fix coq/ltac2#12: Error should name which match cases are unhandled. | Pierre-Marie Pédrot |
| 2017-08-18 | Removing dead code. | Pierre-Marie Pédrot |
| 2017-08-02 | Removing deprecated stuff. | Pierre-Marie Pédrot |
| 2017-07-24 | Turning the ltac2 subfolder into a standalone plugin. | Pierre-Marie Pédrot |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |