diff options
Diffstat (limited to 'compiler/Config.ml')
| -rw-r--r-- | compiler/Config.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index f58ba89b..0475899c 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -304,3 +304,14 @@ let filter_useless_functions = ref true called opaque_defs, of type OpaqueDefs. *) let wrap_opaque_in_sig = ref false + +(** Use short names for the record fields. + + Some backends can't disambiguate records when their field names have collisions. + When this happens, we use long names, by which we concatenate the record + names with the field names, and check whether there are name collisions. + + For backends which can disambiguate records (typically by using the typing + information), we use short names (i.e., the original field names). + *) +let record_fields_short_names = ref false |