diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 49ccb80c..68a67402 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: tacred.ml 13804 2011-01-27 00:41:34Z letouzey $ *) open Pp open Util @@ -216,8 +216,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 -> @@ -481,7 +480,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) @@ -492,7 +490,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 *) |