diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-31 09:09:56 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-31 09:11:27 +0200 |
commit | b994e3195d296e9d12c058127ced381976c3a49e (patch) | |
tree | 8648a92470d27671db9d5e40159a1aec68e8dc9c /checker/mod_checking.ml | |
parent | 7d2ad6ac66abb97819ffbc5ad58c862a84e28775 (diff) |
Checker: avoid using obsolete names from Names
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r-- | checker/mod_checking.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 3ea5ed0d3..c07a35e35 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -18,7 +18,7 @@ let refresh_arity ar = let ctxt, hd = decompose_prod_assum ar in match hd with Sort (Type u) when not (Univ.is_univ_variable u) -> - let ul = Univ.Level.make empty_dirpath 1 in + let ul = Univ.Level.make DirPath.empty 1 in let u' = Univ.Universe.make ul in let cst = Univ.enforce_leq u u' Univ.empty_constraint in let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in @@ -70,7 +70,7 @@ let check_constant_declaration env kn cb = let lookup_module mp env = try Environ.lookup_module mp env with Not_found -> - failwith ("Unknown module: "^string_of_mp mp) + failwith ("Unknown module: "^ModPath.to_string mp) let mk_mtb mp sign delta = { mod_mp = mp; |