diff options
| author | Pierre-Marie Pédrot | 2017-10-30 15:53:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-30 17:12:16 +0100 |
| commit | a997ee7d78d90740b15b58502a1dc5e587b43ee3 (patch) | |
| tree | 0af87e2a77690deda29bec02a978076dd8f89d7e /kernel/type_errors.ml | |
| parent | f18502f32fb25b29cafe26340edbbcedd463c646 (diff) | |
Introducing the change tactic.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions