| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Binding ltac printing functions to the system of generic printing. |  Hugo Herbelin | 2017-11-02 |
| 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 Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |