Why don't the responses from coq-serapi corresponds to type definitions on the coq code?

[brando90]

I was trying to traverse the s-expressions that coq-serapi gives me.

But sometimes there are more arguments than expect. e.g. GenArg should have 2 but coq-serapi gives me 3:

(GenArg raw (OptArg (ExtraArg ltac_selector)) ())

it's type def:

type 'l generic_argument =
| GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument  
A inhabitant of 'level generic_argument is a inhabitant of some type at level 'level, together with the representation of this type.

type raw_generic_argument = rlevel generic_argument

is this an issue with coq serapi or what is going on? @ejgallego

full context: https://proofassistants.stackexchange.com/questions/1601/what-are-generic-arguments-in-coq-and-how-are-they-structured-in-their-ocaml-cod#1601

[ejgallego]

Genargs are very special objects and handled by SerAPI in a special way too. Maybe we can do better, but we'll need to look into it. See ser_genarg.

[ejgallego]

Closed in main