| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-04-11 | Removing the ad-hoc tactic_expr type. | Pierre-Marie Pédrot | |
| This type was actually only used by the debug printer of tactics, and only for atomic tactics. Furthermore, that type was asymmetric, as the underlying tacexpr type was set to be glob_tactic, when the semantics would have required a Val.t type. Furthermore, this type is absent from every contrib I have seen, which hints again in favour of its lack of meaning. | |||
| 2015-02-06 | More efficient Richpp. | Pierre-Marie Pédrot | |
| We build the rich XML at once without generating the printed string. | |||
| 2014-11-10 | Plug the dynamic tags in the Richpp mechanism. | Pierre-Marie Pédrot | |
| 2014-11-05 | lib/RichPp: Rename into Richpp. | Yann Régis-Gianas | |
| printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |