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 --- library/globnames.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'library/globnames.ml') diff --git a/library/globnames.ml b/library/globnames.ml index ea002ef58..06a8f823d 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -155,14 +155,14 @@ let decode_mind kn = if (Dir_path.repr sec_dir) = [] then (Dir_path.make (dir_of_mp mp)),Label.to_id l else - anomaly "Section part should be empty!" + anomaly (Pp.str "Section part should be empty!") let decode_con kn = let mp,sec_dir,l = repr_con kn in match mp,(Dir_path.repr sec_dir) with MPfile dir,[] -> (dir,Label.to_id l) - | _ , [] -> anomaly "MPfile expected!" - | _ -> anomaly "Section part should be empty!" + | _ , [] -> anomaly (Pp.str "MPfile expected!") + | _ -> anomaly (Pp.str "Section part should be empty!") (* popping one level of section in global names *) @@ -178,4 +178,4 @@ let pop_global_reference = function | ConstRef con -> ConstRef (pop_con con) | IndRef (kn,i) -> IndRef (pop_kn kn,i) | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) - | VarRef id -> anomaly "VarRef not poppable" + | VarRef id -> anomaly (Pp.str "VarRef not poppable") -- cgit v1.2.3