Add Gallina bindings for type parameters

This only adds the bindings to function definitions. The parameters
aren't yet passed in function calls, so uses of generic functions won't
work.

glang/coq.go

@@ -765,6 +765,7 @@ func (e FuncLit) Coq(needs_paren bool) string {
 // FuncDecl declares a function, including its parameters and body.
 type FuncDecl struct {
 	Name       string
+	TypeParams []TypeIdent
 	RecvArg    *FieldDecl
 	Args       []FieldDecl
 	ReturnType Type
@@ -810,7 +811,12 @@ func (d FuncDecl) CoqDecl() string {
 	var pp buffer
 	pp.AddComment(d.Comment)
 
-	pp.Add("Definition %s : val :=", d.Name)
+	typeParams := ""
+	for _, t := range d.TypeParams {
+		typeParams += fmt.Sprintf("(%s: go_type) ", t.Coq(false))
+	}
+
+	pp.Add("Definition %s %s: val :=", d.Name, typeParams)
 	func() {
 		pp.Indent(2)
 		defer pp.Indent(-2)

goose.go

@@ -1411,6 +1411,7 @@ func (ctx Ctx) funcDecl(d *ast.FuncDecl) glang.FuncDecl {
 	fd := glang.FuncDecl{Name: d.Name.Name, AddTypes: ctx.Config.TypeCheck}
 	addSourceDoc(d.Doc, &fd.Comment)
 	ctx.addSourceFile(d, &fd.Comment)
+	fd.TypeParams = ctx.typeParamList(d.Type.TypeParams)
 	if d.Recv != nil {
 		if len(d.Recv.List) != 1 {
 			ctx.nope(d, "function with multiple receivers")