Raise an anomaly when looking up unknown constant/inductive

If you have access to a kernel name you also should have the
environment in which it is defined, barring hacks. In order to
disfavor hacks we make the standard lookups raise anomalies so that
people are forced to admit they rely on the internals of the
environment.

We find that hackers operated on the code for side effects, for
finding inductive schemes, for simpl and for Print Assumptions. They
attempted to operate on funind but the error handling code they wrote
would have raised another Not_found instead of being useful.

All these uses are indeed hacky so I am satisfied that we are not
forcing new hacks on callers.

1 files changed, 10 insertions, 6 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 98d66cafa1..2bee2f7a8e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -231,22 +231,26 @@ let fold_inductives f env acc =
 (* Global constants *)
 
 let lookup_constant_key kn env =
-  Cmap_env.find kn env.env_globals.Globals.constants
+  Cmap_env.get kn env.env_globals.Globals.constants
 
 let lookup_constant kn env =
-  fst (Cmap_env.find kn env.env_globals.Globals.constants)
+  fst (lookup_constant_key kn env)
+
+let mem_constant kn env = Cmap_env.mem kn env.env_globals.Globals.constants
 
 (* Mutual Inductives *)
+let lookup_mind_key kn env =
+  Mindmap_env.get kn env.env_globals.Globals.inductives
+
 let lookup_mind kn env =
-  fst (Mindmap_env.find kn env.env_globals.Globals.inductives)
+  fst (lookup_mind_key kn env)
+
+let mem_mind kn env = Mindmap_env.mem kn env.env_globals.Globals.inductives
 
 let mind_context env mind =
   let mib = lookup_mind mind env in
   Declareops.inductive_polymorphic_context mib
 
-let lookup_mind_key kn env =
-  Mindmap_env.find kn env.env_globals.Globals.inductives
-
 let oracle env = env.env_typing_flags.conv_oracle
 let set_oracle env o =
   let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in