diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
| commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
| tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /checker/environ.ml | |
| parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) | |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/environ.ml')
| -rw-r--r-- | checker/environ.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index a0fac3492..0b475ad49 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -111,9 +111,11 @@ let add_constraints c env = let lookup_constant kn env = Cmap_env.find kn env.env_globals.env_constants +let anomaly s = anomaly (Pp.str s) + let add_constant kn cs env = if Cmap_env.mem kn env.env_globals.env_constants then - Printf.ksprintf anomaly "Constant %s is already defined" + Printf.ksprintf anomaly ("Constant %s is already defined") (string_of_con kn); let new_constants = Cmap_env.add kn cs env.env_globals.env_constants in @@ -155,7 +157,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly "Inductive %s is already defined" + Printf.ksprintf anomaly ("Inductive %s is already defined") (string_of_mind kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = user_mind kn,canonical_mind kn in @@ -174,7 +176,7 @@ let add_mind kn mib env = let add_modtype ln mtb env = if MPmap.mem ln env.env_globals.env_modtypes then - Printf.ksprintf anomaly "Module type %s is already defined" + Printf.ksprintf anomaly ("Module type %s is already defined") (string_of_mp ln); let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in let new_globals = @@ -184,7 +186,7 @@ let add_modtype ln mtb env = let shallow_add_module mp mb env = if MPmap.mem mp env.env_globals.env_modules then - Printf.ksprintf anomaly "Module %s is already defined" + Printf.ksprintf anomaly ("Module %s is already defined") (string_of_mp mp); let new_mods = MPmap.add mp mb env.env_globals.env_modules in let new_globals = @@ -194,7 +196,7 @@ let shallow_add_module mp mb env = let shallow_remove_module mp env = if not (MPmap.mem mp env.env_globals.env_modules) then - Printf.ksprintf anomaly "Module %s is unknown" + Printf.ksprintf anomaly ("Module %s is unknown") (string_of_mp mp); let new_mods = MPmap.remove mp env.env_globals.env_modules in let new_globals = |