diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 2 | ||||
| -rw-r--r-- | checker/checker.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/checker/check.ml b/checker/check.ml index 30437e8bd0..b2930d9535 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -329,7 +329,7 @@ let intern_from_file (dir, f) = user_err ~hdr:"intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin - chk_pp (str " (was a vio file) "); + Flags.if_verbose chk_pp (str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) diff --git a/checker/checker.ml b/checker/checker.ml index 167258f8bb..d97ab5409e 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -297,7 +297,7 @@ let explain_exn = function | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints" | UndeclaredUniverse _ -> str"UndeclaredUniverse")) - | Indtypes.InductiveError e -> + | InductiveError e -> hov 0 (str "Error related to inductive types") (* let ctx = Check.get_env() in hov 0 |