diff options
| -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. |