diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2015-03-25 19:06:16 +0100 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2015-03-25 19:11:45 +0100 |
commit | 1bafb18f64ab1c929abfaf9c1b75f691914d9a46 (patch) | |
tree | f62b8ec2d334d23f7214ec4805f05f748f04e0aa /kernel/declareops.ml | |
parent | 5047734648d83890eb4fc4e5cff7ab77d46b48eb (diff) |
Fix vm compiler to refuse to compile code making use of inductives with
more than 245 constructors (unsupported by OCaml's runtime).
Diffstat (limited to 'kernel/declareops.ml')
-rw-r--r-- | kernel/declareops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 48a6098ee..a7051d5c1 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -129,7 +129,7 @@ let subst_const_body sub cb = const_type = type'; const_proj = proj'; const_body_code = - Cemitcodes.subst_to_patch_subst sub cb.const_body_code; + Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code } |