diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index f159395177..cb67d42bdc 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -265,15 +265,12 @@ 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,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 + | Case(ci,u,pms,p,iv,c,br) -> + let acc = Array.fold_left (collrec deep) acc pms in + let acc = Constr.fold (collrec deep) acc (snd 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 + Array.fold_left (fun accu (_, br) -> collrec deep accu br) acc br | App _ -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c | _ -> Constr.fold (collrec true) acc c @@ -369,15 +366,16 @@ 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,iv,c,lf) -> + | Case (ci, u, pms, p, iv, c, lf) -> (* XXX Is ignoring iv OK? *) + let (ci, p, iv, c, lf) = Inductive.expand_case env (ci, u, pms, p, iv, c, lf) in 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',iv,c',lf') + else mkCase (Inductive.contract_case env (ci,p',iv,c',lf')) in (acc'',conclty',sigma, ans) @@ -418,14 +416,15 @@ 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,iv,c,lf) -> + | Case (ci, u, pms, p, iv, c, lf) -> (* XXX is ignoring iv OK? *) + let (ci, p, iv, c, lf) = Inductive.expand_case env (ci, u, pms, p, iv, c, lf) in 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',iv,c',lf') + else mkCase (Inductive.contract_case env (ci,p',iv,c',lf')) in (acc'',conclty',sigma, ans) |