diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-05-16 20:17:18 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-05-16 20:20:25 +0200 |
| commit | c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2 (patch) | |
| tree | cd743dccec87bd991df8cc9944db902d7a546ed5 | |
| parent | d483b7171dafadbe01520bbb6d0c75aa0d6099a7 (diff) | |
Decent error message when a constant is not found
| -rw-r--r-- | kernel/pre_env.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index ba9f30233..ff93d73b6 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -153,7 +153,8 @@ let lookup_constant_key kn env = Cmap_env.find kn env.env_globals.env_constants let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.env_constants) + try fst (Cmap_env.find kn env.env_globals.env_constants) + with Not_found -> Errors.anomaly Pp.(str "Unknown constant " ++ pr_con kn) (* Mutual Inductives *) let lookup_mind kn env = |