diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-02 09:22:37 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-02 09:22:37 +0100 |
| commit | 55d62972391310a71e7bc0eff362fc339455b23b (patch) | |
| tree | 84dfc04b6b25c92ad6e0090310d34db14a37966c /mppa_k1c/abstractbb | |
| parent | 59948b3348964f4b16f408ffe690f2c78ca80959 (diff) | |
| download | compcert-kvx-55d62972391310a71e7bc0eff362fc339455b23b.tar.gz compcert-kvx-55d62972391310a71e7bc0eff362fc339455b23b.zip | |
(Unsafe) coercion of ??bool into bool
Diffstat (limited to 'mppa_k1c/abstractbb')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpConfig.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v index 55931e0f..3d807c4e 100644 --- a/mppa_k1c/abstractbb/Impure/ImpConfig.v +++ b/mppa_k1c/abstractbb/Impure/ImpConfig.v @@ -19,7 +19,7 @@ Module Type ImpureView. *) -(* +(* *) Module UnsafeImpure. Parameter unsafe_coerce: forall {A}, t A -> A. @@ -27,7 +27,7 @@ Module Type ImpureView. Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=x -> mayRet k x. End UnsafeImpure. -*) +(* *) End ImpureView. |