diff options
Diffstat (limited to 'typing/envaux.mli')
| -rw-r--r-- | typing/envaux.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/typing/envaux.mli b/typing/envaux.mli index 91fa4d6040..b893c1412a 100644 --- a/typing/envaux.mli +++ b/typing/envaux.mli @@ -11,13 +11,11 @@ (* *) (***********************************************************************) -(* $Id$ *) - open Format (* Convert environment summaries to environments *) -val env_of_event: Instruct.debug_event option -> Env.t +val env_from_summary : Env.summary -> Subst.t -> Env.t (* Empty the environment caches. To be called when load_path changes. *) |