From 30527475d5c4b03408a8ebadfd7fd4a36f20dff5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 16 May 2017 15:23:39 -0400 Subject: Slightly better type for Interp_InterpToPHOAS --- src/Compilers/Named/InterpretToPHOASInterp.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') 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. -- cgit v1.2.3