diff options
| author | Gaëtan Gilbert | 2019-06-04 14:39:29 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-24 16:33:26 +0200 |
| commit | d13e7e924437b043f83b6a47bfefda69379264b7 (patch) | |
| tree | 06cbf24074c8c8e1803bcaad8c4e297d15149ca9 /pretyping/tacred.ml | |
| parent | 4c779c4fee1134c5d632885de60db73d56021df4 (diff) | |
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.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 6 |
1 files changed, 4 insertions, 2 deletions
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 -> |