diff options
| author | Pierre-Marie Pédrot | 2016-10-25 15:11:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-05-19 15:17:31 +0200 |
| commit | 0c3c2459eae24cc8e87c7c6a4a4e6a1afd171d72 (patch) | |
| tree | beea26ffd64058bedf4157e729503b859f8ef2d1 /Init.v | |
| parent | 94f4ade387013a2e3fe8d1042fbd152088ce1daa (diff) | |
Embedding generic arguments in Ltac2 AST.
Diffstat (limited to 'Init.v')
0 files changed, 0 insertions, 0 deletions