diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 2cc538004..f48734be7 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -141,7 +141,7 @@ let print_env env = in (sign_env ++ db_env) -(*let current_module = ref empty_dirpath +(*let current_module = ref Dir_path.empty let set_module m = current_module := m*) |