aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-30 17:44:42 +0000
committerGitHub2020-12-30 17:44:42 +0000
commitd338a65ce7c4619ecc238c091a409175f5330d8f (patch)
tree590a7d3e0a5c8e1df4f017a1956214354680b690 /kernel/type_errors.mli
parent30f648dc29958add42e7509a9c29f271f768e183 (diff)
parentaed648afd2cf8b09d67fb39c9672b71166089395 (diff)
Merge PR #13682: Fix broken HTML rendering of inference rules (fix #12783).
Reviewed-by: herbelin
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions