diff options
| author | Pierre-Marie Pédrot | 2019-02-04 15:05:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 15:05:40 +0100 |
| commit | 8e73ceb7b4bdb6a17d039b17fd5e44ceffe255a2 (patch) | |
| tree | de5c05721416af1b6c1c2ab03f76ba289fe426c1 /engine/termops.ml | |
| parent | 4fdbf900e11f318f772dd1d81b5fa0a00ccaaa42 (diff) | |
| parent | 0a0d551646ffa105104e418ba7e4274d52cbf8ac (diff) | |
Merge PR #9409: Move non-primitive-record warning to declare_mutual_inductive_with_eliminations
Reviewed-by: ppedrot
Diffstat (limited to 'engine/termops.ml')
0 files changed, 0 insertions, 0 deletions