What exactly is "large elimination"? I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example: 


  impredicative polymorphism + excluded middle + large elimination => false


While I have an intuitive understanding of what it means, I wasn't been able to find or construct a more formal definition of what precisely is "large elimination".

In my understanding, large elimination is when a term t : T is eliminated (destructed) to get a value of type D, where D depends on the value of t.

For example, if vec_bool : nat -&gt; Type is a type constructor for the boolean list of a fixed size with data constructors

nil  : vec_bool 0
cons : forall n:nat, bool -&gt; vec_bool n -&gt; vec_bool (S n)


the following recursive definition performs a large elimination on n:

Fixpoint construct_false_list (n:nat) : vec_bool n :=
   match n with
   | 0      =&gt; nil
   | Succ m =&gt; cons m false (construct_false_list m)
   end.


Is my understanding correct, or am I missing something?
You are incorrect about the definition of large elimination: it refers to the ability to build values of type $\mathrm{Type}$ by eliminating an inductive value. The canonical example:

bool_to_type : bool -&gt; Type := fun b =&gt;
     match b with
         | true =&gt; Unit
         | false =&gt; Empty


Where Unit and Empty are inductive types with 1 and 0 constructors, respectively. Notably, this allows you to prove the proposition $0 \not= 1$, which cannot be proven without this ability.

As noted in another answer (https://cstheory.stackexchange.com/a/21878/3984) a good resource that explains this is the following github repo: https://github.com/FStarLang/FStar/issues/360