aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-02-06 17:11:07 +0100
committerGaëtan Gilbert2020-02-06 21:17:56 +0100
commit53cabaf1e26bfc13e5a45dfeb90ad6a858344c32 (patch)
treee38575cd92b44ce331f0532a5c89dcb387d4e750 /vernac/comProgramFixpoint.ml
parentc38e60243a3cee5d23c76fd78362b7c352c3d8ca (diff)
unsafe_type_of -> get_type_of in Equality.build_injrec
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions