diff options
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 |