- (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
- match coreVarToWeakVar hetmet_brak with
- | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
- | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
- | _ => Prelude_error "IMPOSSIBLE"
- end
- | _ => Prelude_error "IMPOSSIBLE"
- end.
+ (lbinds:list (@CoreBind CoreVar)
+ ) : list (@CoreBind CoreVar) :=
+ coqPassCoreToCore'
+ (coreVarToWeakExprVarOrError hetmet_brak)
+ (coreVarToWeakExprVarOrError hetmet_esc)
+ uniqueSupply
+ lbinds.