Changes in "destruct" tactic (allowing performance improvements):

Changes in "destruct" tactic (allowing performance improvements):
1) discrimination principles are now generated upon definition of an inductive
   type I and recorded as objects I_discr and I_jmdiscr (resp. leibniz and john
   major's principles); in case JMeq wasn't loaded at that time, it is possible
   to explicitly request the definition by means of the command

   discriminator I.

2) destruct uses the aforementioned principle rather than generating a cut at
   each discrimination step

3) destruct performs generalizations using the basic generalize0_tac, rather
   than generalize_tac: this should bring small performance improvements.