/* Reset */
* {
    margin: 0;
    box-sizing: border-box;
}

:root {
    --gap: 1rem;
    --min-skip: 0.25rem;
    --page-w: 29.7cm;
    --page-h: 42cm;
    --font-sans: "Fira Sans", sans;
    --font-monospace: "Iosevka Algr Web", "Iosevka", "Fira Code", monospace;
    --color-rouge: #E30613;
    --color-groseille: #B51F1F;
    --color-leman: #00A79F;
    --color-canard: #007480;
    --color-ardoise: #413D3A;
    --color-perle: #CAC7C7;
    --color-ecmagreen: #2aa198;
    --color-ecmablue: #206CA7;
    --color-ecmayellow: #b58900;
    --color-ecmaorange: #ee8421;
    --color-ecmagray: #cbd7de;
    --hl-literate: #191970;
    --hl-disabled: var(--color-perle);
    --hl-keyword: #B35000;
    --hl-string: var(--color-canard);
    --hl-variable: var(--color-ecmagreen);
}

html {
    line-height: 1.3;
    font-size: 1.05rem;
    font-family: var(--font-sans);
}

p, h3, h4, pre, blockquote {
    margin: 0.5em 0;
}

.katex-display {
    margin: 0 0;
}

blockquote {
    margin-left: 1em;
}

h2 {
    font-size: 1.25em;
}

h2, h3, h4 {
    font-weight: 500;
}

address {
    font-family: var(--font-monospace);
    font-style: initial;
}

pre, code, samp {
    font-family: var(--font-monospace);
}

pre, .esh-standalone, .ecma-box {
    font-size: 0.9em;
    line-height: 1.2;
}

pre.terminal {
    background: var(--color-ardoise);
    color: white;
    padding: 0.5rem;
    border: inset;
}

pre {
    white-space: pre-wrap;
}

code {
    font-variant-ligatures: none;
    white-space-collapse: preserve;
}

code b, code span {
    white-space: pre;
}

pre code {
    font-variant-ligatures: initial;
}

pre code.coq {
    font-feature-settings: "calt" 0, "COQX" 1;
}

code b {
    font-weight: normal;
}

code i {
    color: var(--hl-string);
    font-style: inherit;
}

code var, code b.v {
    color: var(--hl-variable);
    font-style: italic;
}

code .kw {
    color: var(--hl-keyword);
}

code .lit {
    color: var(--hl-literate);
    font-family: var(--font-sans);
    font-style: italic;
    margin: 0.35rem 0 0.15rem 0;
    display: inline-block;
}

code .lit.off {
    opacity: 0.8;
    margin: 0;
}

:is(samp, code) b.ok {
    color: var(--color-leman);
}

:is(samp, code) b.warn {
    color: var(--color-ecmayellow);
}

strong {
    font-weight: 600;
}

ul, ol {
    padding-left: 1.25em;
    /*line-height: 1.7;*/
}

:is(ul, ol) p {
    margin: 0;
}

:is(ul,ol).compact-list {
    line-height: 1.5;
}

.detail {
    font-size: 0.9em;
    text-align: center;
}

.highlight {
    display: block;
    text-align: center;
    font-weight: 500;
}

hr.sep {
    border: none;
}

body {
    max-width: var(--page-w);
    width: 100%;
    display: grid;
    grid-template-rows: auto 1fr auto;
    margin: auto;
}

body > :is(header,footer) {
    display: grid;
    gap: var(--gap);
    padding: var(--gap);
    background: var(--color-ardoise);
    color: white;
    align-items: center;
    justify-items: center;
    text-align: center;
}

body > :is(header,footer) > :first-child {
    justify-self: start;
}

body > :is(header,footer) > :last-child {
    justify-self: end;
}

body > header {
    grid-template-columns: auto 1fr auto;
}

body > header h1 {
    font-size: 1.8rem;
    font-weight: 600;
    text-wrap: balance;
}

/*body > header .author {
    font-size: calc(sqrt(2) * 1em);
}*/

body > header a, body > footer a {
    color: inherit;
    text-decoration: none;
}

body > header img {
    height: 4lh;
}

/*body > header img[src*="qr"] {
    display: none;
}*/

body > header > hgroup {
    text-align: center;
    display: grid;
    grid-gap: 0.5rem;
    line-height: 1;
}

body > header > hgroup > * {
    margin: 0;
}

main {
    display: grid;
    gap: var(--gap);
    padding: var(--gap);
    grid-template-rows: auto auto auto 1fr;
}

main > div {
    display: grid;
    gap: var(--gap);
}

div#background {
    display: grid;
    grid-template-columns: 0.6fr 0.7fr 1fr;
}

main > div#top {
    grid-template-columns: 1fr 1fr;
}

main > div#contribution {
    grid-template-columns: auto 1fr;
}

main > div > article, main > div > div > article, main > div > div > div > article {
    border: thin solid var(--color-ardoise);
}

main article > section, main article > div > section {
    margin: 0.5rem;
}

main > div > article {
    display: grid;
    grid-template-rows: auto 1fr;
}

main > div > article section {
    display: flex;
    flex-grow: 1;
    flex-direction: column;
    gap: var(--min-skip);
    justify-content: space-between;
}

main > div > article section > *,
main > div > article section > * > :first-child {
    margin-top: 0 !important;
}

main > div > article section > *,
main > div > article section > * > :last-child {
    margin-bottom: 0 !important;
}

article > header {
    background: var(--color-canard);
    color: white;
    padding: calc(0.5 * var(--gap));
}

article h3 {
    text-align: center;
}

dd {
    margin-left: 40px;
}

#background section {
    grid-row-gap: unset;
}

#background section > article {
    display: contents;
}

#background section > article h3 {
    margin-bottom: 0;
}

#background section > article:first-child {
    text-align: center;
}

#background section > article:not(:first-child) > div:nth-of-type(1) {
    align-self: end;
}

#background section > article:not(:first-child) > div:nth-of-type(3) {
    align-self: start;
    display: flex;
}

#background .katex-display {
    margin: 0 !important;
}

#background .floating-code code {
    margin-left: 0.5rem;
    float: right;
}

#background .large-operator {
    font-size: 1.5rem;
    text-align: center;
    margin: 0.25rem;
}

#background .rotated-operator {
    transform: rotate(90deg);
}

#quiz .answers {
    text-align: left;
    transform: rotate(180deg);
    font-size: small;
}

#abstract {
    display: grid;
    grid-template-columns: 1fr 5fr;
}

#abstract > article {
    position: relative;
    padding-top: 0.35rlh;
    border: thin solid var(--color-ardoise);
    grid-template-rows: 1fr;
}

#abstract > article h2 {
    font-size: 1rem;
    position: absolute;
    top: -0.5lh;
    left: 0.25lh;
    padding: 0 0.25lh;
    display: inline-block;
    border: thin solid var(--color-ardoise);
    background: white;
}

#abstract .key-point {
    text-align: center;
}

#problem section > * {
    flex-grow: 1;
    align-content: center;
}

#contributions li p {
    display: inline;
}

#abstract #solution .key-point {
    font-size: 2.3rem;
    padding: 0 1rem;
    line-height: 1.1;
    font-weight: 600;
}

#coq pre {
    line-height: 1;
    font-size: 0.85rem;
}

#coq code .lit {
    font-size: 0.8rem;
}

body > footer {
    display: grid;
    grid-template-columns: 1fr auto;
}

body > footer > img {
    height: 1lh;
}

body > footer > .venue {
    text-align: left;
}

table#dialects td {
    border-top: thin solid var(--color-ardoise);
}

table#dialects {
    border-collapse: collapse;
    flex-grow: 1;
}

#priorwork-section {
    display: grid;
    grid-template-rows: auto 1fr;
}

#specs {
    font-size: small;
}

#ecma-highlight {
    width: 100%;
}

#warblre-rocq-icon, #warblre-logo {
    display: inline;
}

#rocq-warblre-linden-logos {
    display: flex;
    justify-content: center;
    align-items: center;
}

#warblre-logo {
    height: 80px;
}

#linden-logo {
    height: 100px;
}

#specs {
    display: grid;
    grid-template-rows: 1fr auto;
    grid-template-columns: 1fr auto 1fr;
    align-items: center;
    text-align: center;
}

cite {
    color: var(--color-canard);
}

#pspace-rocq-proofs {
    display: grid;
    grid-template-columns: 1fr 1fr 1fr;
}

#rocq-proofs-contents {
    display: grid;
    grid-template-columns: .8fr 1fr 1fr 1fr;
}
#rocq-proofs-contents section {
    justify-content: unset;
}

.nomargin {
    margin: 0;
}

#backtracking-tree {
    width: 320px;
}

#pspace-membership section {
    text-align: center;
    align-items: center;
}

#no-negation-membership {
    display: flex;
    flex-direction: column;
    gap: var(--gap);
}

#no-negation {
    flex-grow: 1;
}

#extensions {
    display: grid;
    grid-template-columns: 1fr 1fr 1fr;
}

.center {
    text-align: center;
}

#futurework-references {
    display: flex;
    flex-direction: column;
    gap: var(--gap);
}

#optp section {
    display: flex;
    flex-direction: column;
    gap: 0;
}

.minheight {
    height: 17px;
}

#bottom {
    display: grid;
    grid-template-columns: 1.45fr 1fr;
}

#optp-hardness-completeness {
    display: grid;
    grid-template-columns: 1fr 1fr;
    gap: var(--gap);
}

#references {
    flex-grow: 1;
}

#references section {
    font-size: 8.1pt;
}

#references section h3 {
    font-size: 10pt;
}

@media print {
    body {
        width: var(--page-w);
        height: var(--page-h);
    }

    /*body > header img[src*="qr"] {
        display: block;
    }*/
}

@media (max-width: 27cm) {
    :root {
        --min-skip: 0.5rem;
    }

    pre {
        white-space: pre;
    }

    body {
        width: 100%;
        height: unset;
    }

    main > div {
        display: contents;
    }

    main > div > article > section {
        max-width: 100%;
        overflow-x: auto;
        overflow-y: hidden;
    }

    #background .rotated-operator {
        transform: unset;
    }

    div#background {
        display: flex;
        flex-direction: column;
        align-items: stretch;
        gap: var(--gap);
    }

    #background section > article {
        display: flex;
        flex-direction: row;
        justify-content: center;
        position: relative;
        padding: 0.25rem;
        padding-top: calc(0.35lh + var(--gap));
        gap: var(--min-skip);
    }

    #background section > article:first-child {
        flex-direction: row;
        justify-content: center;
        padding-top: 0.25rem;
        border: none;
    }

    #background section > article:first-child h3 {
        display: none;
    }

    #background section > article,
    #background section > article h3 {
        border: thin solid var(--color-ardoise);
    }

    #background section > article h3 {
        position: absolute;
        top: -0.5lh;
        left: 0.25lh;
        font-size: 1rem;
        padding: 0 0.25lh;
        border: thin solid var(--color-ardoise);
        background: white;
        margin: 0;
    }

    #background section > article > div {
        align-self: center !important;
    }

    #background section > article:first-child > div {
        align-self: baseline !important;
    }

    #abstract, #pspace-rocq-proofs, #rocq-proofs-contents, #bottom {
        display: flex;
        flex-direction: column;
    }
}

@media (max-width: 48rem) {
    #background section > article {
        flex-direction: column;
    }

    #background .rotated-operator {
        transform: rotate(90deg);
    }
}

@media (max-width: 32rem) {
    html {
        font-size: 0.8rem;
    }
}