-(* the WeakType argument in WEBrak/WEEsc is used only when going back *)
-(* from Weak to Core; it lets us dodge a possibly-failing type *)
-(* calculation *)
-| WEBrak : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
-| WEEsc : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
+(* The WeakType argument in WEBrak/WEEsc is used only when going back *)
+(* from Weak to Core; it lets us dodge a possibly-failing type *)
+(* calculation. The CoreVar argument is the GlobalVar for the hetmet_brak *)
+(* or hetmet_esc identifier *)
+| WEBrak : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
+| WEEsc : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr