diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /checker/mod_checking.ml | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r-- | checker/mod_checking.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 3ea5ed0d..7f93e156 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 @@ -26,7 +26,7 @@ let refresh_arity ar = | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = - Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush (); + Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn); let env' = if cb.const_polymorphic then let inst = Univ.make_abstract_instance cb.const_universes 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; |