diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 10 | ||||
| -rw-r--r-- | proofs/logic.ml | 27 |
2 files changed, 20 insertions, 17 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 7fb3a21813..4d148756b4 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -263,7 +263,7 @@ let meta_reducible_instance env evd b = let rec irec u = let u = whd_betaiota env Evd.empty u (* FIXME *) in match EConstr.kind evd u with - | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> + | Case (ci,p,iv,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> let m = destMeta evd (strip_outer_cast evd c) in (match try @@ -272,8 +272,8 @@ let meta_reducible_instance env evd b = if isConstruct evd g || not is_coerce then Some g else None with Not_found -> None with - | Some g -> irec (mkCase (ci,p,g,bl)) - | None -> mkCase (ci,irec p,c,Array.map irec bl)) + | Some g -> irec (mkCase (ci,p,iv,g,bl)) + | None -> mkCase (ci,irec p,iv,c,Array.map irec bl)) | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) -> let m = destMeta evd (strip_outer_cast evd f) in (match @@ -621,8 +621,8 @@ let clenv_cast_meta clenv = else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) - | Case(ci,p,c,br) -> - mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + | Case(ci,p,iv,c,br) -> + mkCase (ci, crec_hd p, map_invert crec_hd iv, crec_hd c, Array.map crec br) | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> u in diff --git a/proofs/logic.ml b/proofs/logic.ml index 07ea2ea572..f159395177 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -265,14 +265,15 @@ let collect_meta_variables c = let rec collrec deep acc c = match kind c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c - | Case(ci,p,c,br) -> - (* Hack assuming only two situations: the legacy one that branches, - if with Metas, are Meta, and the new one with eta-let-expanded - branches *) - let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in - Array.fold_left (collrec deep) - (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c) - br + | Case(ci,p,iv,c,br) -> + (* Hack assuming only two situations: the legacy one that branches, + if with Metas, are Meta, and the new one with eta-let-expanded + branches *) + let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in + let acc = Constr.fold (collrec deep) acc p in + let acc = Constr.fold_invert (collrec deep) acc iv in + let acc = Constr.fold (collrec deep) acc c in + Array.fold_left (collrec deep) acc br | App _ -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c | _ -> Constr.fold (collrec true) acc c @@ -368,14 +369,15 @@ let rec mk_refgoals ~check env sigma goalacc conclty trm = let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> + (* XXX Is ignoring iv OK? *) let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in let sigma = check_conv_leq_goal ~check env sigma trm conclty' conclty in let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm - else mkCase (ci,p',c',lf') + else mkCase (ci,p',iv,c',lf') in (acc'',conclty',sigma, ans) @@ -416,13 +418,14 @@ and mk_hdgoals ~check env sigma goalacc trm = let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) - | Case (ci,p,c,lf) -> + | Case (ci,p,iv,c,lf) -> + (* XXX is ignoring iv OK? *) let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals ~check env sigma goalacc p c in let (acc'',sigma,rbranches) = treat_case ~check env sigma ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm - else mkCase (ci,p',c',lf') + else mkCase (ci,p',iv,c',lf') in (acc'',conclty',sigma, ans) |