aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/type_errors.ml')
-rw-r--r--kernel/type_errors.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f99a026104..c072a368b4 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -70,3 +70,5 @@ let error_ill_formed_rec_body k env str lna i vdefs =
let error_ill_typed_rec_body k env i lna vdefj vargs =
raise (TypeError (k, context env, IllTypedRecBody (i,lna,vdefj,vargs)))
+
+