summaryrefslogtreecommitdiff
path: root/toplevel/topdirs.ml
diff options
context:
space:
mode:
authorThomas Refis <thomas.refis@gmail.com>2018-08-28 17:06:45 +0100
committerThomas Refis <thomas.refis@gmail.com>2018-09-21 11:47:42 -0400
commit67f29d1a18723654ad82a4907baee288567fc25f (patch)
treea63ff5112b1d7cd2f9916e2c440e980a6b0e27c2 /toplevel/topdirs.ml
parent7f3567a63f19775e1d3eb264c5ae1bce820afe34 (diff)
downloadocaml-67f29d1a18723654ad82a4907baee288567fc25f.tar.gz
ident: add an explicit scope field
- Ident.create now takes a scope as argument - added Ident.create_var to use when the scope doesn't matter - the current_time and the current_level are unrelated as of this commit. But one has to remember to bump the level when creating new scopes.
Diffstat (limited to 'toplevel/topdirs.ml')
-rw-r--r--toplevel/topdirs.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/topdirs.ml b/toplevel/topdirs.ml
index 1c629b7fec..69fb6d5391 100644
--- a/toplevel/topdirs.ml
+++ b/toplevel/topdirs.ml
@@ -318,7 +318,6 @@ let match_generic_printer_type desc path args printer_type =
let match_printer_type ppf desc =
let printer_type_new = printer_type ppf "printer_type_new" in
let printer_type_old = printer_type ppf "printer_type_old" in
- Ctype.init_def(Ident.current_time());
try
(match_simple_printer_type desc printer_type_new, false)
with Ctype.Unify _ ->