diff options
| author | Maxime Dénès | 2019-04-04 21:06:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:43 +0200 |
| commit | bf5f0520cf105afb048c6eac5d6de1d3e1a719df (patch) | |
| tree | dfc7afd2f394958a81c5ce33d1422f72b7e6b36b /pretyping/typeclasses.ml | |
| parent | 3b980d937b5adfbae472ed8a13748a451fdf3450 (diff) | |
Remove one call to Global.env in Detyping
One other call still remains, but will require to refactor some
section-handling code.
Diffstat (limited to 'pretyping/typeclasses.ml')
0 files changed, 0 insertions, 0 deletions