diff options
| author | Pierre-Marie Pédrot | 2018-07-26 11:01:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 11:01:34 +0200 |
| commit | 1f083eb5d964ca8740f94ebdec1d69b85b85a6e1 (patch) | |
| tree | 917742ce74d4fcb44699a207a41c2c99a14d6b91 /kernel/nativecode.ml | |
| parent | 6cd6f1edae2e2c7b2aaedd039b39caaf1d50aa9f (diff) | |
| parent | 190ff373ed3728ae816da674ceeae3ba8ffa1919 (diff) | |
Merge PR #7274: Avoiding introducing dependency on the indices of a term which has no matching clauses.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions