diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-03-22 13:55:32 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-03-23 12:45:19 -0400 |
| commit | b0fe1418debe25f3dfe5ac93195a6009b244988e (patch) | |
| tree | da5c78753f3196082e31adb08c1b84e3b40ec520 | |
| parent | 2044c675924d2f63633cbac3c8b5d742526ba4be (diff) | |
Added input var type for clarity
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index ca7340fd5..d72c82e56 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -5371,7 +5371,7 @@ Module Compilers. Definition FromFlat {t} (e : Flat.expr t) : Expr t := let e' := @from_flat t e in fun var => e' var (PositiveMap.empty _). - Definition GeneralizeVar {t} (e : @expr _ t) : Expr t + Definition GeneralizeVar {t} (e : @expr (fun _ => PositiveMap.key) t) : Expr t := FromFlat (to_flat e). End GeneralizeVar. |