diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-29 14:45:30 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-29 14:45:30 -0400 |
commit | 997c187b906170e113a747a197b6c1ee8ba61d05 (patch) | |
tree | f3b44bba9d98928023a5307ac0c450a29c14f76b /src | |
parent | c8e4243676de01bc670957566c6f5921d484a63b (diff) |
Remove a [Check]
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/CommonSubexpressionEliminationInterp.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/Compilers/CommonSubexpressionEliminationInterp.v b/src/Compilers/CommonSubexpressionEliminationInterp.v index 0d7fa1e25..2152b5466 100644 --- a/src/Compilers/CommonSubexpressionEliminationInterp.v +++ b/src/Compilers/CommonSubexpressionEliminationInterp.v @@ -134,8 +134,6 @@ Section symbolic. -Check @symbolize_exprf. - Local Arguments lookupb : simpl never. Local Arguments extendb : simpl never. Lemma interpf_csef G t e1 e2 |