diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 5ca9ac9b4..61cc6b348 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -300,7 +300,6 @@ let safe_init_constant md name () = let fix_proto = safe_init_constant tactics_module "fix_proto" let hide_obligation = safe_init_constant tactics_module "obligation" -let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) let pperror cmd = Errors.errorlabstrm "Program" cmd let error s = pperror (str s) @@ -736,7 +735,6 @@ let not_transp_msg = str "Obligation should be transparent but was declared opaque." ++ spc () ++ str"Use 'Defined' instead." -let warn_not_transp () = ppwarn not_transp_msg let error_not_transp () = pperror not_transp_msg let rec string_of_list sep f = function |