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

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index cb034bdff6..dacef1cb18 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -135,11 +135,13 @@ let lookup_constant_in_impl cst fallback =
       | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".")
 
 let lookup_constant cst =
-  try
-    let cb = Global.lookup_constant cst in
+  let env = Global.env() in
+  if not (Environ.mem_constant cst env)
+  then lookup_constant_in_impl cst None
+  else
+    let cb = Environ.lookup_constant cst env in
     if Declareops.constant_has_body cb then cb
     else lookup_constant_in_impl cst (Some cb)
-  with Not_found -> lookup_constant_in_impl cst None
 
 let lookup_mind_in_impl mind =
   try
@@ -150,8 +152,9 @@ let lookup_mind_in_impl mind =
     anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".")
 
 let lookup_mind mind =
-  try Global.lookup_mind mind
-  with Not_found -> lookup_mind_in_impl mind
+  let env = Global.env() in
+  if Environ.mem_mind mind env then Environ.lookup_mind mind env
+  else lookup_mind_in_impl mind
 
 (** Graph traversal of an object, collecting on the way the dependencies of
     traversed objects *)