diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c9d44e3dc..5b4e8e7cf 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -583,6 +583,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct 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 j + | RCases (loc,po,tml,eqns) -> Cases.compile_cases loc ((fun vtyc env -> pretype vtyc env evdref lvar),evdref) |