From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:35 +0000 Subject: Uniformization of the "anomaly" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/environ.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'checker/environ.ml') 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 = -- cgit v1.2.3