Add a flag to control rewriting under lambdas. Otherwise makes some

rewrite calls fail because an occurence is found under a lambda that
was not found before and there are no adequate morphism declarations to
make the rewrite succeed nor the possibility to give occurences to
rewrite (yet). Only setoid_rewrite will try rewriting under lambda's for
now. Example problem found in a port of the Random library.
Also improved the required_library error message.


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

0 files changed, 0 insertions, 0 deletions