- | DEFAULT => OK ((DEFAULT,nil,e')::rest')
- | LitAlt lit => OK ((LitAlt lit,nil,e')::rest')
- | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),(map coreVarToWeakVar vars),e')::rest')
+ | DEFAULT => OK ((DEFAULT,nil,nil,nil,e')::rest')
+ | LitAlt lit => OK ((LitAlt lit,nil,nil,nil,e')::rest')
+ | DataAlt _ _ _ _ tc' dc => let vars := map coreVarToWeakVar vars in
+ OK (((DataAlt _ dc),
+ (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
+ (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
+ (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
+ e')::rest')