diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-29 14:45:30 -0400 |
|---|---|---|
| committer |  jadep <jade.philipoom@gmail.com> | 2017-06-29 19:49:03 -0400 |
| commit | 90563fe2f8e09dec5fefcab82519f91dc784aba5 (patch) | |
| tree | 0f56ee9a3e54c049464a03b2420ac2cbdd049146 /src | |
| parent | e60833730f6f3f82b50485ba4405bc45f7fabc3d (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 |