diff options
| author | Pierre-Marie Pédrot | 2019-05-11 14:20:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-11 17:36:03 +0200 |
| commit | b83c29a099bde1ea71161c994bbf69b931e6d0f6 (patch) | |
| tree | a9a5c727229bac0dfb06116fe69baf338f982b4a /kernel/nativecode.ml | |
| parent | 1fb2819d57d16196fd8dc7cb49e72b9e1d22758e (diff) | |
Code factorization in elim tactics.
This is just moving code around, so it should not change the semantics.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions