diff options
| author | Pierre-Marie Pédrot | 2016-12-07 14:44:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | d54eacd7b48b9cb0212d5a7cef2ea428469df74a (patch) | |
| tree | 48ac9e31cb4dd31e23095ed7e5e990ff31f81685 /tac2expr.mli | |
| parent | 152b259b7b587ea949dd856b24beaf56466f3f27 (diff) | |
Allow the embedding of Ltac2 terms in constrs via the ltac2:(...) syntax.
Diffstat (limited to 'tac2expr.mli')
0 files changed, 0 insertions, 0 deletions