diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-05-16 22:40:04 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-05-16 22:40:04 +0200 |
| commit | 070fcb00f53062e8bbd57c9398d7a78eba12f641 (patch) | |
| tree | 066db9e871a7fe2fd0d6d9c1ea8e7c2e49c201e0 | |
| parent | 1588a84a71c3df3007296bdafbb29b6a0d15435b (diff) | |
Revert "Decent error message when a constant is not found"
This reverts commit c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2.
| -rw-r--r-- | kernel/pre_env.ml | 3 |
1 files changed, 1 insertions, 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 = |