diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-16 15:23:39 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-16 15:23:39 -0400 |
| commit | 30527475d5c4b03408a8ebadfd7fd4a36f20dff5 (patch) | |
| tree | 103c4c88993bb7d6e8ac3c7ca83316267198f693 /src | |
| parent | 9480dccb77f9e9312c9159a4c7fca8814bc73433 (diff) | |
Slightly better type for Interp_InterpToPHOAS
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Named/InterpretToPHOASInterp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Named/InterpretToPHOASInterp.v b/src/Compilers/Named/InterpretToPHOASInterp.v index 88fb2d8a0..7fe50c994 100644 --- a/src/Compilers/Named/InterpretToPHOASInterp.v +++ b/src/Compilers/Named/InterpretToPHOASInterp.v @@ -82,7 +82,7 @@ Section language. {t} (e : @Named.expr base_type_code op Name t) (Hwf : Named.Wf Context e) v - : Named.interp (Context:=Context _) (interp_op:=interp_op) (ctx:=empty) e v + : Named.Interp (Context:=Context _) (interp_op:=interp_op) e v = Some (Interp interp_op (InterpToPHOAS (Context:=Context) failb e) v). Proof using Type. apply interp_interp_to_phoas; auto. Qed. End all. |