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.

0 files changed, 0 insertions, 0 deletions