Commit to perform double type inference also on inner types.

 * Motivation: the inner sorts computed for the inner types were computed
   by Coq itself. Thus Nijmegen's CProp was exported as Type. To export CProp
   as CProp I have to implement a CProp-aware single type inference.
   To avoid the reimplementation I use double type inference.
 * Known problems: the double type inference algorithm is slower than the
   usual type inference algorithm. Moreover too many types and sorts are
   computed in this way. As a consequence the exportation module is now
   much slower (the exportation time seems to be doubled in the average
   case).

In the future I will try to restore the original performances.


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

0 files changed, 0 insertions, 0 deletions