Services: make the RPC_services predicate more general
In this MR we add two domain parameters to the predicate RPC_service.Valid.t
as parameters for the respective data-encodings. This is required by the service https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/alpha_services#Seed.S.seed_value because one of the encodings of this service is only true on a certain domain.
The downside is that this is very verbose and requires changing other RPC_service.Valid.t
predicates by adding (fun _ => True)
everywhere. I do not know about a good method to have default arguments in Coq, as this domain should probably be (fun _ => True)
by default. A technique would be to use an option type for the domain, which would get reduced to None
instead.
Edited by Guillaume Claret