# What does the tactic constructor do?

I’m trying to understand what does the `constructor` tactic in Coq do. In the documentation, it says “this tactic applies to the goal such that its conclusion is an inductive type”, which I understand it as given the inductive type, the constructor tactic will look for its corresponding constructor to satisfy the goal. How does this work for dependent types? Using this example (which doesn’t make much sense but more to make my point):

`Inductive A : nat -> nat -> Type := | one : A 0 1 | two : A 0 2 | ... | ninetynine : A 9 9.`

and I define the record type:

`Structure foo (n : nat) := { n : nat; m : nat; _ : A n m}.`

and try to prove:

`Theorem p : foo 1.`

In this case `n` is 1 and thus the subgoal will be `A 1 ?m`. Thus any constructor from `ten` to `nineteen` will fit the bill. And depending on how I arrange my constructors above, the tactic `constructor` pick the first one that fits the requirements.

Thus my question here is, what exactly is the tactic `constructor` doing? Is it just merely searching for the constructor that fits the given type? Is there any documentation or OCaml code to explain what `constructor` does?

Thanks

Hi. I think it is simply synonym to first `apply one`, and if it fails `apply two`, and so on until one constructor works. They will be applied in order of definition.
You can already use `constructor 2` to mean `apply two` in this case.

The variant `econstructor` is the same but it will use `eapply`.

What you said does sound right, but `constructor` does slightly more in the sense that before trying the `apply` tactic with the possible terms, saves us the trouble of even finding the type. Would you know of where I can find more details of the `constructor` tactic? Thanks!

Yeah I think it merely looks up the head of the goal and checks it’s an inductive then applies successively the different constructors.
But I don’t know much more than what the doc says, maybe then you would have to look at the ocaml code.