aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Named/DeadCodeEliminationInterp.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Named/DeadCodeEliminationInterp.v')
-rw-r--r--src/Compilers/Named/DeadCodeEliminationInterp.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Named/DeadCodeEliminationInterp.v b/src/Compilers/Named/DeadCodeEliminationInterp.v
index 185a84acd..f822e6e29 100644
--- a/src/Compilers/Named/DeadCodeEliminationInterp.v
+++ b/src/Compilers/Named/DeadCodeEliminationInterp.v
@@ -35,7 +35,7 @@ Section language.
Lemma interp_EliminateDeadCode
t e new_names
- (ctxi_interp : PositiveContext _ _ base_type_code_beq base_type_code_bl)
+ (ctxi_interp : PContext _)
(ctxr_interp : InterpContext)
eout v1 v2 x
: @EliminateDeadCode t e new_names = Some eout