diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-18 18:39:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-18 18:39:31 -0400 |
| commit | 1b18ff42b503c20c460b27e73538a35734052548 (patch) | |
| tree | b1019e979929ef80e60fd5b57b3cb701aebf3905 /src/Reflection/SmartBound.v | |
| parent | b3f96bfa1fe67b41840d79b3377fc02b5b749d85 (diff) | |
Minor simplification in SmartBound
Diffstat (limited to 'src/Reflection/SmartBound.v')
| -rw-r--r-- | src/Reflection/SmartBound.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/SmartBound.v b/src/Reflection/SmartBound.v index 15eeb7b12..56014c7b6 100644 --- a/src/Reflection/SmartBound.v +++ b/src/Reflection/SmartBound.v @@ -34,7 +34,7 @@ Section language. Definition bound_flat_type {t} : interp_flat_type interp_base_type_bounds t -> flat_type - := @SmartFlatTypeMap2 _ _ interp_base_type_bounds (fun t v => Tbase (bound_base_type t v)) t. + := @SmartFlatTypeMap _ interp_base_type_bounds (fun t v => bound_base_type t v) t. Definition bound_type {t} (e_bounds : interp_type interp_base_type_bounds t) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) |