Fixing of guarded_by_constructors completed.

Fixing of guarded_by_constructors completed.
This is the idea of the implementation:
1) The guarded_by_constructors is called on a term which is going to produce
   an inductive type (in every branch).
2) The guarded_by_constructors now has also a parameter which is the list
   of arguments that are applied to the inductive type that the term
   we are cheking is going to produce.
3) Once the constructor is found, its type is "applied" to the list of
   arguments its inductive type is applied to. This operation gives us
   an instantiated constructor type.
4) Depending on the type of every argument in the instantiated constructor
   type, we call either the does_not_occur or the guarded_by_constructors
   on every term the constructor is applied to. In case we call the
   guarded_by_constructors, we also compute the new parameter (list of
   arguments the new inductive type was applied to).

Note that the analysis of the type of the constructors is based very closely
on the analysis of positivy of an inductive type.

Note also that some cases (e.g. a MutCase, a Fix or a CoFix in head position
in the backbone of the type of a constructor) has not been considered and
raises an exception.