diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 17:46:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 17:46:53 +0200 |
| commit | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (patch) | |
| tree | 92ce430c64b7bea374b926d81acc5433d39fdcbb /kernel/csymtable.ml | |
| parent | f79f2b32da8e5e443428d4f642216ddfb404857c (diff) | |
| parent | a18fb93587ccbe32a2edfad38d2e9095f6c8e901 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'kernel/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 3177b5fae..925214899 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -217,17 +217,9 @@ and eval_to_patch env (buff,pl,fv) = eval_tcode tc vm_env and val_of_constr env c = - let (_,fun_code,_ as ccfv) = - try match compile true env c with - | Some v -> v - | None -> assert false - with reraise -> - let reraise = CErrors.push reraise in - let () = print_string "can not compile \n" in - let () = Format.print_flush () in - iraise reraise - in - eval_to_patch env (to_memory ccfv) + match compile true env c with + | Some v -> eval_to_patch env (to_memory v) + | None -> assert false let set_transparent_const kn = () (* !?! *) let set_opaque_const kn = () (* !?! *) |