From d13e7e924437b043f83b6a47bfefda69379264b7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Jun 2019 14:39:29 +0200
Subject: 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.
---
 pretyping/indrec.ml | 28 +++++++++++++---------------
 pretyping/tacred.ml |  6 ++++--
 2 files changed, 17 insertions(+), 17 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index a43549f6c3..0a6c3afd0d 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -620,18 +620,16 @@ let lookup_eliminator env ind_sp s =
   let knc = KerName.make mpc l in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
-  try
-    let cst = Constant.make knu knc in
-    let _ = lookup_constant cst env in
-      GlobRef.ConstRef cst
-  with Not_found ->
-  (* Then try to get a user-defined eliminator in some other places *)
-  (* using short name (e.g. for "eq_rec") *)
-  try Nametab.locate (qualid_of_ident id)
-  with Not_found ->
-    user_err ~hdr:"default_elim"
-      (strbrk "Cannot find the elimination combinator " ++
-       Id.print id ++ strbrk ", the elimination of the inductive definition " ++
-       Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++
-       strbrk " on sort " ++ Sorts.pr_sort_family s ++
-       strbrk " is probably not allowed.")
+  let cst = Constant.make knu knc in
+  if mem_constant cst env then GlobRef.ConstRef cst
+  else
+    (* Then try to get a user-defined eliminator in some other places *)
+    (* using short name (e.g. for "eq_rec") *)
+    try Nametab.locate (qualid_of_ident id)
+    with Not_found ->
+      user_err ~hdr:"default_elim"
+        (strbrk "Cannot find the elimination combinator " ++
+         Id.print id ++ strbrk ", the elimination of the inductive definition " ++
+         Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++
+         strbrk " on sort " ++ Sorts.pr_sort_family s ++
+         strbrk " is probably not allowed.")
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 866c0da555..e8a2189611 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -241,8 +241,10 @@ let invert_name labs l {binder_name=na0} env sigma ref na =
 	let refi = match ref with
 	  | EvalRel _ | EvalEvar _ -> None
 	  | EvalVar id' -> Some (EvalVar id)
-	  | EvalConst kn ->
-	      Some (EvalConst (Constant.change_label kn (Label.of_id id))) in
+          | EvalConst kn ->
+            let kn = Constant.change_label kn (Label.of_id id) in
+            if Environ.mem_constant kn env then Some (EvalConst kn) else None
+        in
 	match refi with
 	  | None -> None
 	  | Some ref ->
-- 
cgit v1.2.3