diff options
Diffstat (limited to 'compiler/Config.ml')
| -rw-r--r-- | compiler/Config.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index bd80769f..ccbb4c75 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -323,3 +323,11 @@ let wrap_opaque_in_sig = ref false information), we use short names (i.e., the original field names). *) let record_fields_short_names = ref false + +(** Parameterize the traits with their associated types, so as not to use + types as first class objects. + + This is useful for some backends with limited expressiveness like HOL4, + and to account for type constraints (like [fn f<T : Foo>(...) where T::bar = usize]). + *) +let parameterize_trait_types = ref false |