diff options
Diffstat (limited to 'mppa_k1c/abstractbb/Impure/ImpCore.v')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpCore.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v index f1abaf7a..508b3f19 100644 --- a/mppa_k1c/abstractbb/Impure/ImpCore.v +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -193,4 +193,4 @@ 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). |