diff options
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 -> |