diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-28 22:40:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-28 22:40:02 -0400 |
| commit | b54e6b8b55c957901cfc8a1504f9cd1b281c5cdd (patch) | |
| tree | 6915248e4f23e602a7c86f9f978dfb504aaf20d1 /src/Reflection/MapInterp.v | |
| parent | 0fb8dfb5e3dd975801d56d5fca0dc2990422350a (diff) | |
Add interp_type_gen_rel_pointwise2, *_gen => *
Diffstat (limited to 'src/Reflection/MapInterp.v')
| -rw-r--r-- | src/Reflection/MapInterp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/MapInterp.v b/src/Reflection/MapInterp.v index 72b37a2d7..bdb7c8a25 100644 --- a/src/Reflection/MapInterp.v +++ b/src/Reflection/MapInterp.v @@ -19,7 +19,7 @@ Section language. Fixpoint mapf_interp {t} (e : @exprf base_type_code interp_base_type1 op var t) : @exprf base_type_code interp_base_type2 op var t := match e in exprf _ _ _ t return exprf _ _ _ t with - | Const tx x => Const (mapf_interp_flat_type_gen f x) + | Const tx x => Const (mapf_interp_flat_type f x) | Var _ x => Var x | Op _ _ op args => Op op (@mapf_interp _ args) | LetIn _ ex _ eC => LetIn (@mapf_interp _ ex) (fun x => @mapf_interp _ (eC x)) |