diff options
| author | Hugo Herbelin | 2014-11-11 12:20:43 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-11 13:32:42 +0100 |
| commit | 34465413bc2d6b3426de783a0d35b968f7ea3b61 (patch) | |
| tree | ebacd66bafed398bea95d893bce49b1cb9e4ed63 /kernel/nativecode.mli | |
| parent | d7e7e9a62fd951b2103d2b6fb9ce2589a16022ca (diff) | |
Renouncing to check only at the end of the call to "apply in" the
absence of remaining dependent evars when several arguments are given.
For simplicity of implementation, checking instead for every step of
the n-ary "apply in".
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions