diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /checker/mod_checking.ml | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 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; |