- (* a ExprCaseBranch contains all the data found in a case branch except the expression itself *)
- Record ExprCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
- { cbi_sacic : @StrongAltConInContext n tc Γ atypes
- ; cbi_vars : vec VV (tagNumValVars (cbi_tag cbi_sacic))
- ; cbi_varstypes := vec2list (vec_zip cbi_vars (cbi_types cbi_sacic))
+ (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
+ Record StrongCaseBranchWithVVs {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
+ { scbwv_scb : @StrongCaseBranch n tc Γ atypes
+ ; scbwv_exprvars : vec VV (saci_numExprVars scbwv_scb)
+ ; scbwv_varstypes := vec2list (vec_zip scbwv_exprvars (scb_types scbwv_scb))