Clean a bit of univ.ml, add credits.
Do not try to match on a subterm that is not closed in find_subterm.
Fix debug printing with primitive projections.

Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.