diff options
| author | Pierre-Marie Pédrot | 2019-10-30 14:18:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-30 14:18:37 +0100 |
| commit | 964e3f409b4db3c682913a4d90394e96453a1274 (patch) | |
| tree | 072e0b588ad881816dde47d9cd8796bbcc0d081b /pretyping | |
| parent | 7634426a7a6de08ff0ea172a0770b9a159b25934 (diff) | |
| parent | d13e7e924437b043f83b6a47bfefda69379264b7 (diff) | |
Merge PR #10303: Raise an anomaly when looking up unknown constant/inductive
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/indrec.ml | 28 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 6 |
2 files changed, 17 insertions, 17 deletions
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 -> |