Test for #3675 on primitive projections.
Granting #3717 (more informative error message on missing arguments for functional induction).
Fixing Functional Induction when applied to an alias (reference manual
for Functional Induction was failing because of minus now an alias).

Knowing that minus is an alias for Sub.nat, there are still two bugs in
Functional Induction (Pierre or Julien?):

"Functional Scheme minus_ind := Induction for minus Sort Prop." is
failing when Nat is not imported.

"functional induction (minus n m)" is failing because looking for
sub_ind while the scheme is named minus_ind.
Fixing doc of Functional Induction.