diff options
| author | Gaëtan Gilbert | 2020-02-06 17:12:07 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 8a8217fe0b1ba8b7548ae648368774105cf21b11 (patch) | |
| tree | ce08b54bcfb9d49872be1eca888b8f47c528820f /vernac/comProgramFixpoint.ml | |
| parent | 53cabaf1e26bfc13e5a45dfeb90ad6a858344c32 (diff) | |
unsafe_type_of -> get_type_of in Equality.inject_if_homogenous_dependent_pair
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions