Need to qualify type constructor in state type declaration

[n-osborne]

When declaring the type of the state, we use the type of the models. They are usually types from the Gospelstdlib (but this is not a gospel obligation).

The code generated does not qualify the type constructors, so list is really from the OCaml standard library and sequence raises an error.

There are two possibilities:

• qualify the type constructors in the type state declaration (this need checking that this is indeed a type from the Gospelstdlib)
• open Ortac_runtime.Gospelstdlib before (we need to chack that this does not raise name capture problem)

[shym]

Oh! That’s ringing a bell! core_type_of_ty_with_subst has a special case for integer (but core_type_of_tysymbol has not, and I don’t know why) which is a really adhoc solution. But now, it turns out that there are more than one such case. And contrary to what term does, those functions don’t rely on Ident.t unicity to ensure the proper name resolution is performed.

I suggest we use for types what we do for value names, ie adding them to the context with the proper full name. Adding integer to the stdlib field of the context (along with all the types of the Gospelstdlib) would be a nicer special case than what is done currently.

Do you agree?