diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 39 |
1 files changed, 23 insertions, 16 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 92617820..64e9ebec 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacred.ml 9762 2007-04-13 12:46:50Z herbelin $ *) +(* $Id: tacred.ml 10135 2007-09-21 14:28:12Z herbelin $ *) open Pp open Util @@ -358,12 +358,11 @@ let reduce_fix_use_function f whfun fix stack = Reduced (contract_fix_use_function f fix,stack') | _ -> NotReducible) -let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) = +let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = match f j with | None -> mkCoFix(j,typedbodies) | Some c -> c in -(* match List.nth names j with Name id -> f id | _ -> assert false in*) let subbodies = list_tabulate make_Fi nbodies in substl (List.rev subbodies) bodies.(bodynum) @@ -372,19 +371,27 @@ let reduce_mind_case_use_function func env mia = | Construct(ind_sp,i) -> let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1), real_cargs) - | CoFix (_,(names,_,_) as cofix) -> - let build_fix_name i = - match names.(i) with - | Name id -> - if isConst func then - let (mp,dp,_) = repr_con (destConst func) in - let kn = make_con mp dp (label_of_id id) in - (match constant_opt_value env kn with - | None -> None - | Some _ -> Some (mkConst kn)) - else None - | Anonymous -> None in - let cofix_def = contract_cofix_use_function build_fix_name cofix in + | CoFix (bodynum,(names,_,_) as cofix) -> + let build_cofix_name = + if isConst func then + let (mp,dp,_) = repr_con (destConst func) in + fun i -> + if i = bodynum then Some func + else match names.(i) with + | Anonymous -> None + | Name id -> + (* In case of a call to another component of a block of + 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 + try match constant_opt_value env kn with + | None -> None + | Some _ -> Some (mkConst kn) + with Not_found -> None + else + fun _ -> None in + let cofix_def = contract_cofix_use_function build_cofix_name cofix in mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false |