diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-08 17:39:28 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-08 17:39:28 +0200 |
| commit | 5619eec808bdb9066c5e26b41956fc4534e103fa (patch) | |
| tree | d4d48a7b4eb53e829f46a3b75193235f4eacd64b /mppa_k1c/abstractbb/Impure/ImpCore.v | |
| parent | 5e06ed3a94dcd7f46b3e087e72e725579d3dd765 (diff) | |
| download | compcert-kvx-5619eec808bdb9066c5e26b41956fc4534e103fa.tar.gz compcert-kvx-5619eec808bdb9066c5e26b41956fc4534e103fa.zip | |
moving iandb from ImpCore to ImpPrelude
Diffstat (limited to 'mppa_k1c/abstractbb/Impure/ImpCore.v')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpCore.v | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v index 9745e35c..55e67608 100644 --- a/mppa_k1c/abstractbb/Impure/ImpCore.v +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -185,11 +185,4 @@ Ltac wlp_xsimplify hint := Create HintDb wlp discriminated. -Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp). - -(* impure lazy andb of booleans *) -Definition iandb (k1 k2: ??bool): ?? bool := - DO r1 <~ k1 ;; - if r1 then k2 else RET false. - -Extraction Inline iandb. (* Juste pour l'efficacité à l'extraction ! *)
\ No newline at end of file +Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file |