aboutsummaryrefslogtreecommitdiff
path: root/kernel/modops.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-20 08:49:36 +0000
committerGitHub2020-11-20 08:49:36 +0000
commitf264aabf59866ae0d18509a7757e69c26e82f508 (patch)
tree6cfa5cca2c0745a54ac0c53c1bf93787d037bd0f /kernel/modops.ml
parent345328cdbcc6e01c884d7e91a72630ee54810d5c (diff)
parent0fff401b5c12a2d0684c8ff4980ebd9716f93905 (diff)
Merge PR #13371: Extend hack to use postponed constraints in retyping to template poly
Reviewed-by: gares Reviewed-by: herbelin
Diffstat (limited to 'kernel/modops.ml')
0 files changed, 0 insertions, 0 deletions