| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-02 | Binding ltac printing functions to the system of generic printing. | Hugo Herbelin | |
| This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |