diff --git a/glang/coq.go b/glang/coq.go
index 4e72fee..f7f6161 100644
--- a/glang/coq.go
+++ b/glang/coq.go
@@ -544,6 +544,8 @@ const (
 	OpLessEqZ
 	OpGreaterEqZ
 
+	OpGallinaAppend
+
 	OpAppend
 	OpMul
 	OpQuot
@@ -565,18 +567,19 @@ type BinaryExpr struct {
 
 func (be BinaryExpr) Coq(needs_paren bool) string {
 	coqBinOp := map[BinOp]string{
-		OpPlus:        "+",
-		OpMinus:       "-",
-		OpEquals:      "=",
-		OpNotEquals:   "≠",
-		OpAppend:      "+",
-		OpMul:         "*",
-		OpQuot:        "`quot`",
-		OpRem:         "`rem`",
-		OpLessThan:    "<",
-		OpGreaterThan: ">",
-		OpLessEq:      "≤",
-		OpGreaterEq:   "≥",
+		OpPlus:          "+",
+		OpMinus:         "-",
+		OpEquals:        "=",
+		OpNotEquals:     "≠",
+		OpGallinaAppend: "++",
+		OpAppend:        "+",
+		OpMul:           "*",
+		OpQuot:          "`quot`",
+		OpRem:           "`rem`",
+		OpLessThan:      "<",
+		OpGreaterThan:   ">",
+		OpLessEq:        "≤",
+		OpGreaterEq:     "≥",
 
 		OpEqualsZ:      "=?",
 		OpLessThanZ:    "<?",
@@ -949,7 +952,7 @@ type VarDecl struct {
 }
 
 func (d VarDecl) CoqDecl() string {
-	return fmt.Sprintf("Definition %s : val := %s.", d.DeclName, d.VarUniqueId.Coq(false))
+	return fmt.Sprintf("Definition %s : string := %s.", d.DeclName, d.VarUniqueId.Coq(false))
 }
 
 func (d VarDecl) DefName() (bool, string) {
diff --git a/goose.go b/goose.go
index 5577b8b..a53d3bc 100644
--- a/goose.go
+++ b/goose.go
@@ -16,6 +16,7 @@ import (
 	"go/constant"
 	"go/token"
 	"go/types"
+	"log"
 	"math/big"
 	"path/filepath"
 	"strconv"
@@ -1338,7 +1339,10 @@ func (ctx *Ctx) funcLit(e *ast.FuncLit) glang.FuncLit {
 
 	ctx.usesDefer = false
 
-	// ctx is by value, so no need to unset this
+	defer func(oldFuncType *types.Signature) {
+		ctx.curFuncType = oldFuncType
+	}(ctx.curFuncType)
+
 	ctx.curFuncType = ctx.typeOf(e.Type).(*types.Signature)
 	fl.Args = ctx.paramList(e.Type.Params)
 	fl.Body = ctx.blockStmt(e.Body, nil)
@@ -1950,7 +1954,6 @@ func (ctx *Ctx) returnStmt(s *ast.ReturnStmt, cont glang.Expr) glang.Expr {
 	var expectedReturnTypes []types.Type
 	if ctx.curFuncType.Results() != nil {
 		for i := range ctx.curFuncType.Results().Len() {
-
 			expectedReturnTypes = append(expectedReturnTypes, ctx.curFuncType.Results().At(i).Type())
 		}
 	}
@@ -1992,6 +1995,12 @@ func (ctx *Ctx) returnStmt(s *ast.ReturnStmt, cont glang.Expr) glang.Expr {
 			}
 		}
 
+		if len(unconvertedReturnValues) != len(expectedReturnTypes) {
+			log.Print(len(unconvertedReturnValues), len(expectedReturnTypes))
+			log.Print(ctx.curFuncType.Results())
+			ctx.nope(s, "bug")
+		}
+
 		for i, e := range unconvertedReturnValues {
 			exprs = append(exprs, ctx.handleImplicitConversion(e.n, e.t, expectedReturnTypes[i], e.e))
 		}
@@ -2353,7 +2362,7 @@ func (ctx *Ctx) globalVarDecl(d *ast.GenDecl) []glang.Decl {
 				DeclName: name.Name,
 				VarUniqueId: glang.BinaryExpr{
 					X:  glang.GallinaIdent("global_id'"),
-					Op: glang.OpPlus,
+					Op: glang.OpGallinaAppend,
 					Y:  glang.StringLiteral{Value: name.Name},
 				},
 			})