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 /library/nametab.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 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 46d8dcc3f..6829e9431 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -172,7 +172,7 @@ let rec push_exactly uname o level tree = function let ptab' = push_exactly uname o (level-1) mc path in mktree tree.path (ModIdmap.add modid ptab' tree.map) | [] -> - anomaly "Prefix longer than path! Impossible!" + anomaly (Pp.str "Prefix longer than path! Impossible!") let push visibility uname o tab = @@ -312,7 +312,7 @@ struct let equal d1 d2 = Int.equal (Dir_path.compare d1 d2) 0 let to_string = Dir_path.to_string let repr dir = match Dir_path.repr dir with - | [] -> anomaly "Empty dirpath" + | [] -> anomaly (Pp.str "Empty dirpath") | id :: l -> (id, l) end |