diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 802a32b0e7..83e41a63ec 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -548,7 +548,9 @@ let rec execute env cstr = | Construct c -> cstr, type_of_constructor env c - | Case (ci,p,iv,c,lf) -> + | Case (ci, u, pms, p, iv, c, lf) -> + (** FIXME: change type_of_case to handle the compact form *) + let (ci, p, iv, c, lf) = expand_case env (ci, u, pms, p, iv, c, lf) in let c', ct = execute env c in let iv' = match iv with | NoInvert -> NoInvert @@ -563,7 +565,7 @@ let rec execute env cstr = let lf', lft = execute_array env lf in let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr - else mkCase(ci',p',iv',c',lf') + else mkCase (Inductive.contract_case env (ci',p',iv',c',lf')) in cstr, t @@ -720,11 +722,6 @@ let judge_of_inductive env indu = let judge_of_constructor env cu = make_judge (mkConstructU cu) (type_of_constructor env cu) -let judge_of_case env ci pj iv cj lfj = - let lf, lft = dest_judgev lfj in - let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in - make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t - (* Building type of primitive operators and type *) let type_of_prim_const env _u c = |