diff options
| author | letouzey | 2011-04-06 11:38:31 +0000 |
|---|---|---|
| committer | letouzey | 2011-04-06 11:38:31 +0000 |
| commit | 7a7a09378e492b5b2dc87e3a8e502e842ca1faf5 (patch) | |
| tree | 3a71b586ed39ea4c81eb12c81044ae8007c8d57a /kernel/type_errors.ml | |
| parent | f8e8ffa4b7c42f6c53126d284c0bfbf8a992bc89 (diff) | |
Add 'Existing Instances' declaration to declare multiple instances at once.
This is useful, for example, in declaring the projection of the dependent
record bundled form of an unbundled typeclass.
Patch submitted by Tom Prince
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13956 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions