diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 15:27:40 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 15:27:40 +0200 |
| commit | 16e8902f08ed1bf7481a2e7f21b5ebb6c6c81814 (patch) | |
| tree | 02a3a82a972d6d955414d07ad7f112fbd74c46b0 /powerpc/ConstpropOp.vp | |
| parent | 1f004665758e26e6e48d13f5702fe55af8944448 (diff) | |
| download | compcert-kvx-16e8902f08ed1bf7481a2e7f21b5ebb6c6c81814.tar.gz compcert-kvx-16e8902f08ed1bf7481a2e7f21b5ebb6c6c81814.zip | |
Update PowerPC port (not tested yet)
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) |