Fixing a small bug in computing implicit arguments in (co-)fixpoints.

The recursive functions and their binders were not pushed in the right
order for implicit arguments.

Additionally, we avoid calling push_name_env both for interpreting the
type of each component of a (co-)fixpoint and for interpreting again the
body of each component of a (co-)fixpoint because it may have
side-effects (in the glob file). So we instead remember the part of
its action on implicit arguments to replay it functionally.

0 files changed, 0 insertions, 0 deletions