diff options
| author | Pierre-Marie Pédrot | 2021-03-12 19:20:46 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-12 19:27:49 +0100 |
| commit | c8a051cc9d85ef425b780a8454e8567e423171b4 (patch) | |
| tree | 8c46122bf3b3d2c9e013114bafe39b342b741e02 /kernel/nativelibrary.mli | |
| parent | 5645beeab5801e86704c97b2cc8687b01c14acb8 (diff) | |
Use the new API to prevent retyping of Ltac2 variable quotations.
Fixes #12785: Ltac2 Performance Overhead.
Diffstat (limited to 'kernel/nativelibrary.mli')
0 files changed, 0 insertions, 0 deletions