# What are Generic Arguments in Coq and how are they structured in their OCaml code?

**URL:** <https://discourse.rocq-prover.org/t/what-are-generic-arguments-in-coq-and-how-are-they-structured-in-their-ocaml-code/1732>\
**Category:** Developing plugins\
**Created:** [July 14, 2022, 7:20pm UTC](https://discourse.rocq-prover.org/t/what-are-generic-arguments-in-coq-and-how-are-they-structured-in-their-ocaml-code/1732 "2022-07-14T19:20:25Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [July 14, 2022, 7:20pm UTC](https://discourse.rocq-prover.org/t/what-are-generic-arguments-in-coq-and-how-are-they-structured-in-their-ocaml-code/1732/1 "2022-07-14T19:20:25Z")

</div>

I was trying to figure out why it seems that in a [Coq generic argument](https://coq.github.io/doc/v8.11/api/coq/Genarg/index.html#type-raw_generic_argument) there seems to be 3 arguments to the constructor [`GenArg`](https://coq.github.io/doc/v8.11/api/coq/Genarg/index.html#type-generic_argument.GenArg) when according to me there should only be 2 (plus one of the argument seems to skip to other constructors I was expecting based on the OCaml algebraic data type code [e.g. `OptArg`](https://coq.github.io/doc/v8.11/api/coq/Genarg/index.html#type-genarg_type.OptArg)).

I see from coq-serapi:

```auto
((GenArg raw (OptArg (ExtraArg ltac_selector)) ())
          (GenArg raw (OptArg (ExtraArg ltac_info)) ())
          (GenArg raw (ExtraArg tactic)
           (TacArg
            ((v
              (TacCall
               ((v
                 (((v (Ser_Qualid (DirPath ()) (Id ___hole)))
                   (loc
                    (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                      (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 8)))))
                  ( (ConstrMayEval
                    (ConstrTerm
                     ((v
                       (CPrim (Numeral SPlus ((int 0) (frac "") (exp "")))))
                      (loc
                       (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                         (line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))))) )))
                (loc
                 (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                   (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
             (loc
              (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
          (GenArg raw (ExtraArg ltac_use_default) false)) ))))

```

focusing on the first one in the [raw\_generic\_argument](https://coq.github.io/doc/v8.11/api/coq/Genarg/index.html#type-raw_generic_argument) list:

```auto
(GenArg raw (OptArg (ExtraArg ltac_selector)) ()

```

we see we have this weird word `raw` that according to me should NOT be there because look at the type definition for [raw\_generic\_argument](https://coq.github.io/doc/v8.11/api/coq/Genarg/index.html#type-raw_generic_argument):

```auto
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

```

the constructor [`GenArg` should only take 2 things](https://coq.github.io/doc/v8.11/api/coq/Genarg/index.html#type-generic_argument.GenArg). But the argument I showed takes 3 things – the last one being unit, perhaps?

Can someone explain we what’s going on?

* * *

In addition, the second argument `(OptArg (ExtraArg ltac_selector))` seems completely off too. We know `'l` is `rlevel`. We should have `('a rlevel) abstract_argument_type` as the first argument (which seems to be the second one according to the s-expression I pasted. The `abstract_argument_type` has constructors:

```auto
type (_, _) abstract_argument_type =
| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type

```

but none appear…which is super puzzling to me. There are 3 options and nothing else. So why does it randomly skip to the constructor `OptArg` [corresponding to `gen_arg_type`](https://coq.github.io/doc/v8.11/api/coq/Genarg/index.html#type-genarg_type)?

* * *

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