diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 986825f25c..9669acc230 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -493,7 +493,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let j = pretype tycon env isevars lvar (RCases (loc, None, [c], [p])) - in j + (* 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 |