coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-05-21	Fixing a small bug in computing implicit arguments in (co-)fixpoints.	Hugo Herbelin
	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.