ocaml-gospel/gospel

The string type is still defined in the Structure module as a built in gospel type but it is not used as model for any OCaml type. Indeed, the model for OCaml strings is char sequence (which makes perfect sense). This can be a bit confusing for an unaware user as one will have some type checking errors when using Gospel strings to talk about OCaml ones. For instance, this piece of specification, though quite natural, won't type check, accepting the person type declaration but failing on the ensures clause: (*@ type person = { firstname: string; lastname: string } *) type t (*@ model : person *) val make : string -> string -> t (*@ t = make firstname lastname ensures t = { firstname; lastname } *) A possible bonus would be to parse "example" as a char sequence.