diff options
| author | Pierre-Marie Pédrot | 2019-06-08 15:08:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:38:35 +0200 |
| commit | c3efcc501e140a74a948513a0e45223e4d5b521c (patch) | |
| tree | b0b2254addfe26859f73a93ae859ab4a04912e7b /kernel/nativelambda.ml | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
Adding the ability to transfer Ltac2 variables to Ltac1 quotations.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions