Fix a bug found by B. Grégoire when declaring morphisms in module

types. Change (again) the semantics of bindings and the binding modifier
! in typeclasses. Inside [ ], implicit binding where only parameters
need to be given is the default, use ! to use explicit binding, which is
equivalent to regular bindings except for generalization of free
variables. Outside brackets (e.g. on the right of instance
declarations),  explicit binding is the default, and implicit binding
can be used by adding ! in front. This avoids almost every use of ! in
the standard library and in other examples I have.


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

0 files changed, 0 insertions, 0 deletions