diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:45:27 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:59:00 +0530 |
| commit | 8309a98096facfba448c9d8d298ba3903145831a (patch) | |
| tree | 38a09851cb687921193b4368a93eed34ccd55a58 /kernel/nativecode.ml | |
| parent | 58153a5bc59bbde6534425d66a2fe5d9943eb44b (diff) | |
Correct restriction of vm_compute when handling universe polymorphic
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 433e2c505..66577fecc 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1772,7 +1772,7 @@ let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> begin match cb.const_body with - | Def t -> + | Def t when not cb.const_polymorphic -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code"); @@ -1902,8 +1902,8 @@ let compile_mind_deps env prefix ~interactive let rec compile_deps env sigma prefix ~interactive init t = match kind_of_term t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind - | Const (c,u) -> - let c = get_allias env c in + | Const c -> + let c,u = get_allias env c in let cb,(nameref,_) = lookup_constant_key c env in let (_, (_, const_updates)) = init in if is_code_loaded ~interactive nameref |