diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f9fcdb7b6..83381710d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -582,23 +582,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in { uj_val = v; uj_type = p } - - | RLetPattern (loc, c, p) -> - (* Just use cases typing *) - let j = - pretype tycon env evdref lvar - (RCases (loc, None, [c], [p])) - in - (* Change case info *) - let j' = match kind_of_term j.uj_val with - Case (ci, po, c, br) -> - let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in - { j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) } - | _ -> j - in j' - | RCases (loc,po,tml,eqns) -> - Cases.compile_cases loc + | RCases (loc,sty,po,tml,eqns) -> + Cases.compile_cases loc sty ((fun vtyc env -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) |