Fixes in new Morphisms files.

- Use a notation for predicate instead of a
definition (better pretty-printing this way, and no delta
problem!).
- Correct inadvertent import of Coq.Program.Program which sets
implicit arguments for left,right and so on. Should fix the contribs
that used to compile. 
- Correct normalization_tac to do normalization of "inverse"
signatures. Add a missing instance, and name the existing ones.


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

0 files changed, 0 insertions, 0 deletions