diff options
Diffstat (limited to 'mppa_k1c/abstractbb/Impure/ImpConfig.v')
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpConfig.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/abstractbb/Impure/ImpConfig.v b/mppa_k1c/abstractbb/Impure/ImpConfig.v index e49a4611..dd9785b5 100644 --- a/mppa_k1c/abstractbb/Impure/ImpConfig.v +++ b/mppa_k1c/abstractbb/Impure/ImpConfig.v @@ -82,4 +82,4 @@ Extract Inlined Constant bind => "(|>)". Extract Constant t "" => "". (* This weird directive extracts [t] as "'a" instead of "'a t" *) Extraction Inline t. -Global Opaque t.
\ No newline at end of file +Global Opaque t. |