diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index db57503f6..187ea4478 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -1007,5 +1007,6 @@ type clos_infos = fconstr infos let create_clos_infos ?(evars=fun _ -> None) flgs env = create (fun _ -> inject) flgs env evars +let oracle_of_infos { i_env } = Environ.oracle i_env let unfold_reference = ref_value_cache |