diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-11 14:53:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-11 15:11:58 +0200 |
| commit | 7ec643712e5376bc2a3f71d4673947b94c60415f (patch) | |
| tree | 71264003c5b5a42f23f1253b31a0508bb5f1b291 /pretyping/typeclasses.mli | |
| parent | 5ab7efb4d32b05b3ab967d46bc59a0bc853bbae2 (diff) | |
Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility with inversion
Diffstat (limited to 'pretyping/typeclasses.mli')
0 files changed, 0 insertions, 0 deletions