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, 5 insertions, 7 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 00559206ee..e846b17aa0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -302,8 +302,8 @@ let lift_constant c =
 let push_private_constants env eff =
   let eff = side_effects_of_private_constants eff in
   let add_if_undefined env eff =
-    try ignore(Environ.lookup_constant eff.seff_constant env); env
-    with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env
+    if Environ.mem_constant eff.seff_constant env then env
+    else Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env
   in
   List.fold_left add_if_undefined env eff
 
@@ -598,8 +598,8 @@ let inline_side_effects env body side_eff =
   (** First step: remove the constants that are still in the environment *)
   let filter e =
     let cb = (e.seff_constant, e.seff_body) in
-    try ignore (Environ.lookup_constant e.seff_constant env); None
-    with Not_found -> Some (cb, e.from_env)
+    if Environ.mem_constant e.seff_constant env then None
+    else Some (cb, e.from_env)
   in
   (* CAVEAT: we assure that most recent effects come first *)
   let side_eff = List.map_filter filter (SideEffects.repr side_eff) in
@@ -750,9 +750,7 @@ let translate_direct_opaque env kn ce =
   { cb with const_body = OpaqueDef c }
 
 let export_side_effects mb env (b_ctx, eff) =
-      let not_exists e =
-        try ignore(Environ.lookup_constant e.seff_constant env); false
-        with Not_found -> true in
+      let not_exists e = not (Environ.mem_constant e.seff_constant env) in
       let aux (acc,sl) e =
         if not (not_exists e) then acc, sl
         else e :: acc, e.from_env :: sl in