diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 21:01:17 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 21:01:17 +0200 |
commit | 104681e5db184659a36762e0776cef133d70455b (patch) | |
tree | d0ad556679cde1526bb947ca15ee0bf740c2fc34 /mppa_k1c/abstractbb/Impure/ImpCore.v | |
parent | fd2c2a0bdf723dce559567324711a3127ce0582e (diff) | |
parent | 4032ed3192424a23dbb0a4f3bd2a539b22625168 (diff) | |
download | compcert-kvx-104681e5db184659a36762e0776cef133d70455b.tar.gz compcert-kvx-104681e5db184659a36762e0776cef133d70455b.zip |
Merge branch 'mppa-ternary' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ternary
Diffstat (limited to 'mppa_k1c/abstractbb/Impure/ImpCore.v')
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpCore.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v index 6eb0c5af..9745e35c 100644 --- a/mppa_k1c/abstractbb/Impure/ImpCore.v +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -132,6 +132,7 @@ Proof. destruct x; simpl; auto. Qed. + (* Tactics MAIN tactics: @@ -184,4 +185,11 @@ Ltac wlp_xsimplify hint := Create HintDb wlp discriminated. -Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file +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 |