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/Compilers/CommonSubexpressionEliminationInterp.v | |
| parent | c8e4243676de01bc670957566c6f5921d484a63b (diff) | |
Remove a [Check]
Diffstat (limited to 'src/Compilers/CommonSubexpressionEliminationInterp.v')
| -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 |