diff options
| author | Matej Kosik | 2015-12-16 15:24:18 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-18 15:58:14 +0100 |
| commit | 9e8a9ab17d4467a4aa40f31eaef0800703d31418 (patch) | |
| tree | 6f6d7e49900b90d9dc9823b24fce7d355c038aed /pretyping/typeclasses_errors.ml | |
| parent | e4423ce78823ad9dd8c726e31de712e67a91893a (diff) | |
COMMENTS: added to some variants of "Globalnames.global_reference" type.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions