Does the order of declarations in an inductive type matter? I was wondering if the order of declarations of an inductive type can matter.

For example in Coq you can define Nat either by:

Inductive Nat :=
  | O : Nat
  | S : Nat -&gt; Nat.


or

Inductive Nat :=
  | S : Nat -&gt; Nat
  | O : Nat.


This will perhaps change the order of the parameters in the automatically generated eliminator, but that’s not a big deal.

What I’m wondering is if it is possible to write a declaration like

Inductive typewhereordermatters :=
  | cons1 : type1
  | cons2 : type2.


where type2 is a dependent type, depending on cons1? (and in this case, write the declarations in the other order would not have any meaning, because type2 would be referring to cons1 which does not exists yet).
The order does not matter. I cannot think of a case where it would. As Andrej Bauer points out in a comment, if you change the order the result is canonically isomorphic to the original. 
One case cannot depend on another case. The elements of the sum represent a choice, so it doesn't make sense that the choice taken depends upon a choice that is not taken.