X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=1761b834e98fc7a6cfcfccc6d95929552bc1286d;hp=ad1dee7faf013a1238ad37eb858befcfe3072e63;hb=97552c1a6dfb32098d4491951929ab1d4aca96a0;hpb=92e148ed7a7b0068cf2029537b019a88a7b07d43 diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index ad1dee7..1761b83 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -209,7 +209,7 @@ Section HaskStrongToWeak. Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ) (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : ???WeakExpr := - match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with + match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with uniqM f => f us >>= fun x => OK (snd x) end.