A parameter, when discharged, carries its original visibility with it into each place it is bound. This meant that in definitions such as list, either the element type was always implicit and nil was awkward, or it was always explicit and cons was awkward. The unsatisfactory workaround was to make it explicit, rename the cons constructor, then define cons as a lambda term with the correct visibility. Some appearances of the renamed constructor were inevitable.
Hence conditional visibility, indicated by `?'. When a conditionally visible variable is bound, its visibility is made implicit if it occurs in a subsequent pi-bound argument of its range type, and explicit otherwise. Consequently, [A?Prop][a?A]a is translated as [A|Prop][a:A]a, since in its type {A|Prop}A->A, the A occurs in the argument type immediately left of the ->.
The same holds for discharging, so that
Inductive [list:SET] Parameters [A?SET] Constructors [nil:list] [cons:A->list->list]; Discharge A;leaves A explicit for list and nil, but implicit for cons and list_elim.
The library definitions of list and vector have been updated to use this new feature. This afftects the visibility of the type parameter for list_elim, vcons, vect_elim and so forth, hence some proof scripts may break. Most of the problems arising from this can be fixed by replacing list_elim with list_elim| and likewise for the others, so that the first argument supplied is taken as the implicit parameter.