aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-16 17:14:37 +0000
committerGitHub2020-11-16 17:14:37 +0000
commit04b25a7635e796ad05ef7db537883594a5144a56 (patch)
tree75e0efa3f2e1b924dbe54dc1736fd9f28346b7c1 /engine
parent29dc0d5b8951bb467bb2cc473a90e8feaadbb9b8 (diff)
parent6f31beeaaaf99306d206964e1bd3e966b0475023 (diff)
Merge PR #12873: Unification: A type-checking fix in imitation + an error locating fix
Reviewed-by: gares
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions