From 070fcb00f53062e8bbd57c9398d7a78eba12f641 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 May 2014 22:40:04 +0200 Subject: Revert "Decent error message when a constant is not found" This reverts commit c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2. --- kernel/pre_env.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index ff93d73b6..ba9f30233 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -153,8 +153,7 @@ let lookup_constant_key kn env = Cmap_env.find kn env.env_globals.env_constants let lookup_constant kn env = - try fst (Cmap_env.find kn env.env_globals.env_constants) - with Not_found -> Errors.anomaly Pp.(str "Unknown constant " ++ pr_con kn) + fst (Cmap_env.find kn env.env_globals.env_constants) (* Mutual Inductives *) let lookup_mind kn env = -- cgit v1.2.3