diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index bd875cf68b..04feae35d8 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -356,8 +356,7 @@ let make_case_or_project env sigma indt ci pred c branches = let IndType (((ind,_),_),_) = indt in let projs = get_projections env ind in match projs with - | None -> - mkCase (ci, pred, make_case_invert env indt ci, c, branches) + | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches))) | Some ps -> assert(Array.length branches == 1); let na, ty, t = destLambda sigma pred in @@ -749,6 +748,6 @@ let control_only_guard env sigma c = in let rec iter env c = check_fix_cofix env c; - EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c + EConstr.iter_with_full_binders env sigma EConstr.push_rel iter env c in iter env c |