diff options
Diffstat (limited to 'powerpc/ConstpropOp.vp')
| -rw-r--r-- | powerpc/ConstpropOp.vp | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index e768e4a9..403a7a77 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -20,8 +20,6 @@ Require Import ValueDomain. (** * Converting known values to constants *) -Parameter symbol_is_external: ident -> bool. (**r See [SelectOp] *) - Definition const_for_result (a: aval) : option operation := match a with | I n => Some(Ointconst n) |