diff options
| author | Pierre-Marie Pédrot | 2016-12-02 14:31:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | 2dc3175916f3968d4cdba9af140fbc2667ff70a5 (patch) | |
| tree | 5f0b9dd0c677d1dc259d44459a199c6cbf7ff1a0 /tac2expr.mli | |
| parent | 0c3c2459eae24cc8e87c7c6a4a4e6a1afd171d72 (diff) | |
Allowing to include Coq terms in Ltac2 using the constr:(...) syntax.
Diffstat (limited to 'tac2expr.mli')
0 files changed, 0 insertions, 0 deletions