diff options
| -rw-r--r-- | kernel/names.ml | 6 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 7 |
3 files changed, 9 insertions, 5 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index d31c4f93fa..d53a7aa300 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -234,7 +234,7 @@ type constructor = inductive * int let constant_of_kn kn = (kn,kn) let constant_of_kn_equiv kn1 kn2 = (kn1,kn2) -let make_con mp dir l = ((mp,dir,l),(mp,dir,l)) +let make_con mp dir l = constant_of_kn (mp,dir,l) let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) let canonical_con con = snd con let user_con con = fst con @@ -246,6 +246,10 @@ let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++ let eq_constant (_,kn1) (_,kn2) = kn1=kn2 let debug_string_of_con con = string_of_kn (fst con)^"'"^string_of_kn (snd con) +let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl = + if lbl = l1 && lbl = l2 then con + else ((mp1,dp1,lbl),(mp2,dp2,lbl)) + let con_modpath con = modpath (fst con) let mind_modpath mind = modpath (fst mind) diff --git a/kernel/names.mli b/kernel/names.mli index b5e71b9d4b..bf1fca87f3 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -143,6 +143,7 @@ val user_con : constant -> kernel_name val canonical_con : constant -> kernel_name val repr_con : constant -> module_path * dir_path * label val eq_constant : constant -> constant -> bool +val con_with_label : constant -> label -> constant val string_of_con : constant -> string val con_label : constant -> label diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 99776367bb..de87e5029a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -214,8 +214,7 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - let (mp,dp,_) = repr_con kn in - Some (EvalConst (make_con mp dp (label_of_id id))) in + Some (EvalConst (con_with_label kn (label_of_id id))) in match refi with | None -> None | Some ref -> @@ -468,7 +467,6 @@ let reduce_mind_case_use_function func env sigma mia = | CoFix (bodynum,(names,_,_) as cofix) -> let build_cofix_name = if isConst func then - let (mp,dp,_) = repr_con (destConst func) in let minargs = List.length mia.mcargs in fun i -> if i = bodynum then Some (minargs,func) @@ -479,7 +477,8 @@ let reduce_mind_case_use_function func env sigma mia = mutual inductive, try to reuse the global name if the block was indeed initially built as a global definition *) - let kn = make_con mp dp (label_of_id id) in + let kn = con_with_label (destConst func) (label_of_id id) + in try match constant_opt_value env kn with | None -> None (* TODO: check kn is correct *) |