1. added code to handle the inclusion of inductive types and constructors in

   parameters.
2. however, the code is still not working if the parameters are referenced
   later on in the module signature. To fix this the representation of
   terms must be changed to unify references to constants, inductive types and
   constructors.
3. thus the code above is prefixed by an error that suggest to the user how
   to avoid the problem right now. Note: the above code has not been commented
   out to keep it in synch with the other changes in the kernel. However, it
   is dead code for now.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6600 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions