diff options
| author | Pierre-Marie Pédrot | 2013-12-22 15:38:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-22 15:38:25 +0100 |
| commit | db33ec1898dacbcd398c38e0a6535be931ed5fb3 (patch) | |
| tree | 549db57c24866b68bcf42a1a3884feeecb42863f /kernel/nativecode.ml | |
| parent | 455d5ee36dc36cbf094ddccf43059cddceedcd1f (diff) | |
Notation variables are now taken into account as possible ltac bound variables
when internalizing a term.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions