diff options
Diffstat (limited to 'src')
| -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. |