aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/mod_checking.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r--checker/mod_checking.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index bc4ea7c69..ebe44997d 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -35,7 +35,7 @@ let check_constant_declaration env kn cb =
let _ = infer_type envty ty in
(match body_of_constant cb with
| Some bd ->
- let j = infer env' (force_constr bd) in
+ let j = infer env' bd in
conv_leq envty j ty
| None -> ())
| PolymorphicArity(ctxt,par) ->