diff options
author | 2015-07-15 13:15:50 +0200 | |
---|---|---|
committer | 2015-07-15 13:15:50 +0200 | |
commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /kernel/csymtable.ml | |
parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r-- | kernel/csymtable.ml | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index ed8b0a6d..b29f06c6 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -148,14 +148,17 @@ let rec slot_for_getglobal env (kn,u) = with NotEvaluated -> (* Pp.msgnl(str"not yet evaluated");*) let pos = - match Cemitcodes.force cb.const_body_code with - | BCdefined(code,pl,fv) -> - if Univ.Instance.is_empty u then - let v = eval_to_patch env (code,pl,fv) in - set_global v - else set_global (val_of_constant (kn,u)) - | BCallias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant (kn,u)) in + match cb.const_body_code with + | None -> set_global (val_of_constant (kn,u)) + | Some code -> + match Cemitcodes.force code with + | BCdefined(code,pl,fv) -> + if Univ.Instance.is_empty u then + let v = eval_to_patch env (code,pl,fv) in + set_global v + else set_global (val_of_constant (kn,u)) + | BCallias kn' -> slot_for_getglobal env kn' + | BCconstant -> set_global (val_of_constant (kn,u)) in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (Ephemeron.create pos); pos @@ -210,7 +213,9 @@ and eval_to_patch env (buff,pl,fv) = and val_of_constr env c = let (_,fun_code,_ as ccfv) = - try compile env c + try match compile true env c with + | Some v -> v + | None -> assert false with reraise -> let reraise = Errors.push reraise in let () = print_string "can not compile \n" in |