aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorJason Gross2016-06-18 14:44:04 -0700
committerJason Gross2016-06-18 14:44:04 -0700
commit6bfdd3efccf852dad84b393b9272293434d65725 (patch)
tree6d71600f3ecc31bfc0c254d0cb22868774c59314 /kernel/type_errors.ml
parentb2495b2326083776f9b15355acac77cde73545e1 (diff)
Fix the build on Windows
This fixes bug #4828 (https://coq.inria.fr/bugs/show_bug.cgi?id=4828).
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions