/* dterm-rocq: Rocq drawn as structure (rocq_draw.pl), over nanofil's
   dterm.css, which sets the terms; formal.html loads it too, for the
   Rocq in its prose (code.rq). Inductive types are tables of their
   constructors, relations and theorems are inference rules, proofs fold
   under their statements. */

article.dterm-rocq { max-width: 64rem; }
.dterm-rocq { container-type: inline-size; }
article.guide:has(.rq-layout) { container-type: inline-size; }
.rq-layout:not([hidden]) {
  display: flex; flex-wrap: wrap; align-items: center; gap: 0.3rem 0.5rem;
  margin: 0 0 0.8rem; padding: 0.3rem 0;
  border-block: 1px solid var(--rule); font-size: 0.85rem;
}
.rq-layout label { font-weight: 650; }
.rq-layout select { font: inherit; color: var(--ink); background: var(--paper, white); padding: 0.2rem; border: 1px solid var(--muted); border-radius: 0; }
.rq-layout select:focus-visible { outline: 2px solid var(--accent); outline-offset: 3px; }
/* The index: no sidebar, which would only repeat its list. Each file is
   its name and size beside its header's first sentence, or over it on a
   phone. */
main.dterm-page > article.rq-index { grid-column: 1 / -1; max-width: 60rem; }
.rq-index h2.rq-dir {
  margin: 1.8rem 0 0; padding: 0 0 0.3rem; border-top: 0;
  font: 600 0.8rem/1.3 var(--mono, ui-monospace, monospace); color: var(--muted);
}
.rq-index h2.rq-dir a { color: inherit; }
.rq-index h2.rq-dir a:hover { color: var(--accent); }
dl.rq-files {
  display: grid; grid-template-columns: max-content minmax(0, 1fr);
  margin: 0; font-size: 0.94rem; line-height: 1.45;
}
dl.rq-files > :is(dt, dd) { margin: 0; padding: 0.5rem 0; border-top: 1px solid var(--rule); min-width: 0; }
dl.rq-files dt { padding-right: 1.2rem; }
dl.rq-files dt a { font-weight: 650; overflow-wrap: anywhere; }
.rq-file-meta { display: block; color: var(--muted); font-size: 0.74rem; font-variant-numeric: tabular-nums; white-space: nowrap; }
dl.rq-files dd { overflow-wrap: break-word; }
dl.rq-files dd code { font-size: 0.84em; overflow-wrap: anywhere; }
@media (max-width: 700px) {
  dl.rq-files { grid-template-columns: minmax(0, 1fr); }
  dl.rq-files dt { display: flex; flex-wrap: wrap; align-items: baseline; gap: 0 0.6rem; padding: 0.5rem 0 0.1rem; }
  .rq-file-meta { white-space: normal; }
  dl.rq-files dd { border-top: 0; padding-top: 0; }
}
/* A long path as a page's title breaks where it must. */
.dterm-rocq h1.source-title { overflow-wrap: anywhere; }
:is(.dterm-rocq, code.rq) { --ty: #6b3d7a; --lem: #7a4a14; }

:is(.dterm-rocq, code.rq) .ty { color: var(--ty); }
:is(.dterm-rocq, code.rq) .ty.def, :is(.dterm-rocq, code.rq) .lem.def, :is(.dterm-rocq, code.rq) .a.def, :is(.dterm-rocq, code.rq) .f.def { font-weight: 700; }
:is(.dterm-rocq, code.rq) .ty.def { color: var(--ty); }
:is(.dterm-rocq, code.rq) .lem { color: var(--lem); }
:is(.dterm-rocq, code.rq) .lem.def { color: var(--ink); }
:is(.dterm-rocq, code.rq) .g { color: var(--ink); }
.dterm-rocq a.a, .dterm-rocq a.ty, .dterm-rocq a.f, .dterm-rocq a.lem, .dterm-rocq a.g { text-decoration: none; }
.dterm-rocq a.a:hover, .dterm-rocq a.ty:hover, .dterm-rocq a.f:hover, .dterm-rocq a.lem:hover { text-decoration: underline; }
:is(.dterm-rocq, code.rq) .q { color: var(--accent); font-weight: 600; margin-right: 0.12em; }
:is(.dterm-rocq, code.rq) .qsep { margin-left: 0.02em; }
:is(.dterm-rocq, code.rq) .defeq { color: var(--muted); }
:is(.dterm-rocq, code.rq) .scope { color: var(--muted); font-size: 0.8em; }
:is(.dterm-rocq, code.rq) .explicit > .at { color: var(--muted); }
:is(.dterm-rocq, code.rq) .module-name { font-weight: 700; color: var(--ink); }
:is(.dterm-rocq, code.rq) .binder { white-space: nowrap; }
.dterm-rocq .c.sig > .args.binders { border-width: 0; padding-inline: 0; margin-left: 0.3em; }
:is(.dterm-rocq, code.rq) .c.quant > .args { border: 0; padding: 0; margin-left: 0.2em; }
:is(.dterm-rocq, code.rq) .paren.binder, :is(.dterm-rocq, code.rq) .braces.binder { margin: 0 0.05em; }
:is(.dterm-rocq, code.rq) .c.app > .args { border-width: 0; padding-inline: 0; margin-left: 0.3em; border-radius: 0; }
:is(.dterm-rocq, code.rq) .args.recbr { border-width: 0; padding-inline: 0; }
:is(.dterm-rocq, code.rq) .args.recbr::before { content: "{|"; color: var(--paren); margin-right: 0.25em; }
:is(.dterm-rocq, code.rq) .args.recbr::after { content: "|}"; color: var(--paren); margin-left: 0.25em; }
:is(.dterm-rocq, code.rq) .args.recbr.curly::before { content: "{"; }
:is(.dterm-rocq, code.rq) .args.recbr.curly::after { content: "}"; }
:is(.dterm-rocq, code.rq) .c.tuple > .args { border-width: 0 var(--paren-stroke); }
:is(.dterm-rocq, code.rq) .bar { color: var(--muted); }
:is(.dterm-rocq, code.rq) .kw { font-size: 0.72em; }
/* (elt:=A), a named argument, and p~0~1, a positive's binary digits. */
:is(.dterm-rocq, code.rq) .rq-arg-name { color: var(--muted); }
:is(.dterm-rocq, code.rq) .rq-bits { color: var(--muted); font-size: 0.85em; }
/* Inline in a document's prose, a term keeps to its line. */
code.rq .c, code.rq .args, code.rq .arg { white-space: nowrap; }
.dterm .prose code.rq :is(.c.quant, .c.quant > .args, .c.quant > .args > .arg) { white-space: normal; }
.dterm-rocq [data-v].lit { background: color-mix(in srgb, var(--var) 14%, transparent); border-radius: 3px; }

/* Iris as its papers set it: masks, fractions and step-indices are small
   scripts on their arrows; a big operator carries its binders under it;
   proof mode patterns are hypothesis names among quiet marks. */
:is(.dterm-rocq, code.rq) :is(sup, sub).rq-mask, :is(.dterm-rocq, code.rq) .op sub { font-size: 0.68em; line-height: 0; }
:is(.dterm-rocq, code.rq) .rq-upd-arrow, :is(.dterm-rocq, code.rq) .rq-pointsto { white-space: nowrap; }
:is(.dterm-rocq, code.rq) .rq-big-op { font-size: 1.2em; line-height: 1; }
:is(.dterm-rocq, code.rq) .rq-big-binds { font-size: 0.6em; font-weight: 400; color: var(--ink); white-space: nowrap; }
:is(.dterm-rocq, code.rq) .rq-big-binds .op { margin-inline: 0.08em; }
:is(.dterm-rocq, code.rq) .rq-triple-brace { color: var(--accent); }
:is(.dterm-rocq, code.rq) .rq-post > .op { color: var(--paren); }
:is(.dterm-rocq, code.rq) .rq-wp-head { white-space: nowrap; margin-right: 0.15em; }
:is(.dterm-rocq, code.rq) .rq-wp-head > .kw { font-size: 0.78em; letter-spacing: 0.03em; }
:is(.dterm-rocq, code.rq) .rq-proj { color: var(--muted); font-size: 0.85em; }
:is(.dterm-rocq, code.rq) .rq-const { color: var(--atom); }
:is(.dterm-rocq, code.rq) .rq-pure > .op { color: var(--accent); }
:is(.dterm-rocq, code.rq) .rq-ipm .v { font-style: italic; }
:is(.dterm-rocq, code.rq) .rq-ipm-mark { margin-inline: 0.03em; }

/* Directives: a quiet line each. */
.rq-dirs { margin: 0.6rem 0 1rem; font-size: 0.86rem; color: var(--muted); }
.rq-dir .module { color: var(--atom); }
.dterm-rocq .clause.rq-module-def { margin: 0.2rem 0; }

/* Headings from (** * Title *). */
.dterm-rocq h2.rq-sec { margin: 2.2rem 0 0.6rem; font-size: 1.3rem; }
.dterm-rocq h3.rq-sec { margin: 1.6rem 0 0.4rem; font-size: 1.05rem; }
.rq-subtitle { font-size: 1.15rem; font-weight: 650; margin: 0 0 0.4rem; }
.rq-doc { margin: 0.9rem 0 0.3rem; max-width: 44rem; }
.rq-doc .prose p { margin: 0 0 0.4rem; overflow-wrap: break-word; }
.dterm-rocq .note { font-style: normal; }
.dterm-rocq code.term.rq { font: inherit; font-size: 0.96em; background: none; padding: 0; }
.dterm-rocq a.ref.pl code { color: var(--accent); }

/* Sentences. */
.dterm-rocq .clause { margin: 0.4rem 0 0.9rem; }
.rq-ind { margin: 0.4rem 0 1rem; scroll-margin-top: 3rem; }
.dterm-rocq .rq-ind-head { margin: 0 0 0.15rem; }
table.rq-ctors, table.rq-fields { border-collapse: collapse; margin: 0 0 0 0.6em; font-size: 0.95rem; max-width: 100%; }
table.rq-ctors td, table.rq-fields td { padding: 0.1rem 0.8rem 0.1rem 0; vertical-align: baseline; }
table.rq-ctors td.bar { color: var(--muted); padding-right: 0.5rem; }
table.rq-ctors td.ctor, table.rq-fields td.field-name { white-space: nowrap; }
table.rq-ctors td.ctor-aside, table.rq-fields td.field-aside { max-width: 24rem; }
table.rq-ctors td.ctor-aside .aside, table.rq-fields td.field-aside .aside { margin: 0; }
table.rq-ctors tr:target, table.rq-fields tr:target, .rq-rule:target, .clause:target {
  background: color-mix(in srgb, var(--accent) 7%, transparent);
}
table.rq-ctors tr.note td, table.rq-fields tr.note td { padding-top: 0.4rem; }
.rq-body { margin: 0.15rem 0 0 0.8em; max-width: 100%; overflow-x: auto; }
.dterm-rocq .aside { font-style: normal; }

/* match as a table of patterns and results; let as a binding over its body. */
.rq-match .match-head { margin-bottom: 0.1em; }
.dterm-rocq .cases { width: max-content; max-width: 100%; }
.dterm-rocq .cases.ztry { max-width: none; }
.dterm-rocq .cases.stack { width: auto; grid-template-columns: max-content minmax(0, 1fr); }
.cases.match { margin-left: 0.6em; }
/* A match too wide for its table (dterm.js stacks it) is each pattern
   over its result, the result led by ⇒, not a conditional's labels. */
.dterm-rocq .cases.match.stack { grid-template-columns: 1em minmax(0, 1fr); column-gap: 0.3em; }
.dterm-rocq .cases.match.stack > .case:not(.plain) > .cond::before { content: none; }
.dterm-rocq .cases.match.stack > .case > .cond > .goals { grid-column: 1 / -1; }
.dterm-rocq .cases.match.stack > .case:not(.plain) > .then::before {
  content: "⇒"; color: var(--accent); font-size: 1em; text-transform: none; letter-spacing: 0;
}
.cases.match > .case > .arrow { font-weight: 500; }
.rq-let > .let-body, .rq-fun > .fun-body { margin-top: 0.1em; }
.rq-let > .let-value { margin-left: 1.5em; }
.rq-app > .app-tail { padding-left: 1.2em; }
.rq-app > .app-args { display: grid; grid-template-columns: minmax(0, 1fr); row-gap: 0.2em; padding-left: 1.2em; margin-top: 0.1em; }
.rq-fun > .fun-body { margin-left: 1.2em; }
.rq-tuple { border-inline: var(--paren-stroke) solid var(--paren); border-radius: 0.6em; padding-inline: 0.4em; }
.tuple-part + .tuple-part::before { content: ","; color: var(--muted); }

/* Inference rules: premises over a line, the conclusion under it, the
   rule's name beside the line. */
.rules { display: grid; gap: 0.9rem; margin: 0.3rem 0 0 1.2em; }
.rule { display: inline-grid; grid-template-columns: minmax(0, 1fr); max-width: 100%; }
.rule-vars { color: var(--muted); font-size: 0.88rem; margin-bottom: 0.15rem; }
.rule-vars .v.def { color: var(--var); font-weight: 500; }
/* Without the term planner, wide premises must wrap inside the rule too. */
.premises { display: grid; grid-template-columns: minmax(0, 1fr); row-gap: 0.1em; padding: 0 0.6em; }
.rule-line {
  display: flex; align-items: center; gap: 0.6em;
  margin: 0.15em 0; min-height: 0.3em;
}
.rule-line::before { content: ""; flex: 1 1 auto; border-top: 1.2px solid var(--ink); opacity: 0.7; }
.rule-name { font-size: 0.85rem; overflow-wrap: anywhere; }
.rule-concl { padding: 0 0.6em; }
.rule-concl.alone { display: flex; flex-wrap: wrap; gap: 0.8em; align-items: baseline; padding: 0; }
.rule .goal { min-width: 0; }
.rq-thm { margin: 0.8rem 0 1.2rem; scroll-margin-top: 3rem; }
/* A long declaration name (find_emit_bug_reporting_address_start) has
   no space to break at; it breaks where it must rather than push the
   page sideways. */
.rq-thm-head { margin-bottom: 0.2rem; overflow-wrap: anywhere; }
.rq-thm > .rule { margin-left: 1.2em; }
.rq-axiom > .rq-thm-head .kw { color: var(--accent); }

/* Proofs fold under their statements. */
details.rq-proof { margin: 0.25rem 0 0 1.2em; font-size: 0.85rem; }
details.rq-proof > summary { cursor: pointer; color: var(--muted); list-style: none; }
details.rq-proof > summary::-webkit-details-marker { display: none; }
details.rq-proof > summary::before { content: "▸ "; }
details.rq-proof[open] > summary::before { content: "▾ "; }
.proof-count { font-size: 0.85em; }
.proof-steps { margin: 0.2rem 0 0 0.9em; padding-left: 0.6em; border-left: 2px solid var(--rule); }
.dterm-rocq .tac { display: grid; grid-template-columns: max-content minmax(0, 1fr); gap: 0.15em; margin: 0.1rem 0; font-size: 0.9rem; line-height: 1.4; }
.tac .bullet { display: inline-block; min-width: 1.1em; color: var(--accent); white-space: nowrap; }
.rq-focus { min-width: 0; margin-left: 0.45em; padding-left: 0.35em; border-left: 1px solid var(--rule); }
.rq-braced { border-left-color: var(--paren); border-radius: 0.5em; padding-block: 0.1em; }
.tactic { white-space: normal; }
/* Tactic control flow is structure; each atomic tactic uses dterm's
   existing application/operator printer, including its Gallina terms. */
.rq-ltac { scroll-margin-top: 3rem; }
.rq-tac-inline { display: block; }
.tactic .c.app > .args { padding-block: 0; }
.tactic .rq-tac-args { padding: 0; margin: 0; border: 0; background: none; }
.rq-tac-clause > .kw { color: var(--muted); font-weight: 500; }
.rq-tac-chain > .op { color: var(--accent); }
.rq-intro-or, .rq-intro-and, .rq-tac-alternatives { padding-inline: 0.22em; }
.rq-rewrite { white-space: nowrap; }
.rq-tac-match, .rq-tac-choices, .rq-tac-group, .rq-tac-seq { display: block; min-width: 0; }
.rq-tac-seq { display: grid; grid-template-columns: 0.6em minmax(0, 1fr); gap: 0 0.2em; }
.rq-tac-left { grid-column: 1 / -1; }
.rq-tac-prefix, .rq-tac-select, .rq-tac-choices { display: grid; grid-template-columns: max-content minmax(0, 1fr); gap: 0 0.3em; }
.rq-tac-head, .rq-tac-end { display: block; }
.rq-tac-options { display: grid; margin-left: 0.4em; }
.rq-tac-option { display: grid; grid-template-columns: 0.7em minmax(0, 1fr); gap: 0.2em; }
.rq-tac-option:first-child > .rq-choice-bar { visibility: hidden; }
.rq-choice-bar, .rq-tac-sep, .rq-selector { color: var(--muted); }
.rq-tac-pattern { display: block; }
.rq-tac-pattern > .arg { margin-right: 0.2em; }
.rq-token-group { border: 0; padding: 0; background: none; }
.rq-equation { min-width: 0; max-width: 100%; }

/* The proof is a reading surface, not an embedded IDE. The existing
   term printer still owns every goal's line breaks and name links. */
details.rq-captured { margin: 0.25rem 0 1rem; font-size: 0.9rem; }
.rq-captured > summary { padding: 0.2rem 0; }
.rq-captured .proof-invite { color: var(--accent); font-weight: 650; }
.rq-captured .proof-count { margin-left: 0.4rem; }
.rq-explorer { border-block: 1px solid var(--rule); padding: 0.4rem 0; }
/* Do not style the large snapshot tree while its disclosure is closed.
   The modal moves the explorer out of this direct-child relationship. */
.rq-captured:not([open]) > .rq-explorer { display: none; }
html:has(.rq-dialog[open]) { overflow: hidden; }
.rq-dialog { box-sizing: border-box; width: calc(100vw - 1.5rem); max-width: none; height: calc(100dvh - 1.5rem); max-height: none; padding: 0 0.7rem; border: 1px solid var(--rule); color: var(--ink); background: var(--paper, white); container-type: inline-size; overflow: hidden; }
.rq-dialog[open] { display: grid; grid-template-rows: auto minmax(0, 1fr); }
.rq-dialog::backdrop { background: #0008; }
/* One header row on desktop: name, navigation, layout, close. */
.rq-dialog-head { display: flex; flex-wrap: wrap; align-items: center; gap: 0.3rem 0.6rem; padding-block: 0.35rem; border-bottom: 1px solid var(--rule); background: var(--paper, white); }
.dterm-rocq .rq-dialog-head h2 { flex: 0 1 auto; margin: 0; padding: 0; border: 0; min-width: 0; font-family: inherit; font-size: 1rem; font-weight: 650; line-height: 1.3; white-space: nowrap; overflow: hidden; text-overflow: ellipsis; }
.rq-dialog-head :is(button, select) { font: inherit; font-size: 0.8rem; padding: 0.2rem 0.4rem; background: transparent; color: var(--ink); border: 1px solid var(--rule); cursor: pointer; }
.rq-dialog-head button { font-size: 1.2rem; line-height: 1; }
.rq-dialog .rq-proof-controls { padding: 0; flex-wrap: nowrap; }
.rq-dialog-head select { margin-left: auto; }
.rq-dialog .rq-proof-controls [data-move] { min-width: 2rem; }
.rq-dialog .rq-proof-controls .rq-compare { margin-left: 0.3rem; }
/* On desktop the script and the selected state are two panes that scroll
   on their own, under the header; the source script folds below them. */
.rq-dialog .rq-explorer { display: grid; grid-template-rows: minmax(0, 1fr) auto; min-height: 0; border: 0; padding: 0; overflow: hidden; }
.rq-dialog .rq-walk { grid-template-columns: minmax(16rem, 0.45fr) minmax(0, 1fr); grid-template-rows: minmax(0, 1fr); align-items: stretch; gap: 0; min-height: 0; }
.rq-dialog :is(.rq-timeline, .rq-states) { min-height: 0; overflow-y: auto; overscroll-behavior: contain; }
.rq-dialog .rq-timeline { padding: 0.3rem 0.4rem 0.6rem 0; }
.rq-dialog .rq-states { padding: 0.3rem 0 0.8rem 0.8rem; }
.rq-dialog .rq-script { margin: 0; padding-block: 0.2rem; }
.rq-dialog .rq-script[open] { max-height: 35vh; overflow-y: auto; }
/* The selected tactic is highlighted beside its state; only several
   open goals, or the comparison's earlier state, need a heading. */
.rq-dialog .rq-state-heading h3 { display: none; }
.rq-dialog .rq-state-heading:not(:has(.rq-goal-count)) { display: none; }
.rq-dialog .rq-state-heading { justify-content: flex-end; border: 0; padding: 0; }
.rq-proof-controls:not([hidden]) { display: flex; align-items: center; flex-wrap: wrap; gap: 0.3rem; padding-bottom: 0.4rem; }
.rq-proof-controls button { font: inherit; font-size: 0.8rem; padding: 0.25rem 0.4rem; background: var(--paper, white); color: var(--ink); border: 1px solid var(--rule); border-radius: 0; cursor: pointer; }
.rq-proof-controls button:hover:not(:disabled), .rq-proof-controls button[aria-pressed=true] { border-color: var(--accent); color: var(--accent); }
.rq-proof-controls button:disabled { opacity: 0.45; cursor: default; }
.rq-proof-controls .rq-position { font-size: 0.75rem; color: var(--muted); font-variant-numeric: tabular-nums; }
.rq-proof-controls .rq-compare { margin-left: auto; }
.rq-captured :is(button, summary):focus-visible { outline: 2px solid var(--accent); outline-offset: 2px; }
.rq-walk { display: grid; grid-template-columns: minmax(0, 13rem) minmax(0, 1fr); gap: 0.6rem; align-items: start; }
.rq-walk:has(.rq-timeline[hidden]) { grid-template-columns: minmax(0, 1fr); }
.rq-timeline { padding: 0 0.4rem 0 0; border-right: 1px solid var(--rule); }
.dterm-rocq .rq-step-link { display: grid; grid-template-columns: max-content minmax(0, 1fr); gap: 0.15em; width: 100%; margin: 0; border: 0; border-left: 2px solid transparent; border-radius: 0; background: transparent; color: var(--muted); text-align: left; padding: 0.12rem 0.25rem; font: inherit; font-size: 0.85rem; line-height: 1.4; overflow-wrap: anywhere; white-space: normal; cursor: pointer; }
.rq-step-link > .bullet { min-width: 0.9em; white-space: nowrap; }
.rq-step-name { grid-column: 1 / -1; }
.dterm-rocq .rq-step-link:hover { background-color: color-mix(in srgb, var(--accent) 5%, transparent); color: var(--ink); }
.dterm-rocq .rq-step-link[aria-current=step] { color: var(--accent); border-left-color: var(--accent); background-color: color-mix(in srgb, var(--accent) 8%, transparent); }
.rq-states, .rq-snapshot { min-width: 0; }
.rq-states { container: rq-states / inline-size; }
.rq-snapshot { scroll-margin-top: 5rem; }
.rq-snapshot + .rq-snapshot:not([hidden]) { margin-top: 0.6rem; }
.rq-state-heading { display: flex; align-items: baseline; gap: 0.4rem; padding-bottom: 0.2rem; border-bottom: 1px solid var(--rule); }
.rq-state-heading h3.clause { flex: 1; min-width: 0; margin: 0; font: inherit; font-size: 0.9rem; line-height: 1.5; overflow-wrap: anywhere; }
.rq-state-heading .bullet { color: var(--accent); margin-right: 0.4em; }
.rq-goal-count { flex-shrink: 0; font-size: 0.72rem; color: var(--muted); }
.rq-changes { margin: 0.2rem 0; color: #38664d; font-size: 0.75rem; }
.rq-changes:empty { display: none; }
.rq-proof-goal.clause { padding: 0; margin: 0.3rem 0; min-width: 0; }
.rq-context { display: grid; grid-template-columns: fit-content(40%) minmax(0, 1fr); row-gap: 0.05rem; column-gap: 0.5rem; line-height: 1.4; }
.rq-hyp { display: grid; grid-template-columns: subgrid; grid-column: 1 / -1; align-items: baseline; padding: 0 0.25rem; border-left: 2px solid transparent; }
.rq-hyp.wide > .rq-hyp-type { grid-column: 2 / -1; }
/* A wide pane sets short hypotheses side by side, in columns whose names
   and types still align; long ones keep a whole row. Reading order is
   Rocq's, left to right. */
@container rq-states (min-width: 38rem) {
  .rq-context { grid-template-columns: repeat(2, max-content minmax(0, 1fr)); }
  .rq-hyp:not(.wide) { grid-column: span 2; padding-right: 1rem; }
}
@container rq-states (min-width: 58rem) {
  .rq-context { grid-template-columns: repeat(3, max-content minmax(0, 1fr)); }
}
@container rq-states (min-width: 80rem) {
  .rq-context { grid-template-columns: repeat(4, max-content minmax(0, 1fr)); }
}
.rq-hyp:has(.rq-hyp-type > div) { align-items: start; }
.rq-hyp-names { font-size: 0.85rem; }
.rq-hyp-names, .rq-hyp .rq-unparsed { overflow-wrap: anywhere; }
.rq-hyp > .rq-unparsed { grid-column: 1 / -1; }
.rq-hyp-type.goal { min-width: 0; }
.rq-proof-goal div.goal { overflow-x: auto; max-width: 100%; font-size: 0.92rem; }
.rq-conclusion { display: grid; grid-template-columns: max-content minmax(0, 1fr); gap: 0.4rem; align-items: baseline; border-left: 2px solid transparent; padding: 0.2rem 0.25rem; }
.rq-context + .rq-conclusion { border-top: 1px solid var(--rule); margin-top: 0.3rem; }
.rq-turnstile { color: var(--muted); }
/* The proof mode's contexts as Iris prints them: persistent hypotheses
   over a rule marked □, spatial ones over a rule marked ∗, the goal. */
/* Rocq's own context over the proof mode's, as Iris's ==== line. */
.rq-context:not(.rq-ipm-context) + :is(.rq-ipm-context, .rq-ipm-rule) { margin-top: 0.3rem; padding-top: 0.25rem; border-top: 3px double var(--rule); }
.rq-ipm-rule { display: flex; align-items: center; gap: 0.3rem; color: var(--muted); font-size: 0.8rem; line-height: 1; margin: 0.15rem 0; }
.rq-ipm-rule::before { content: ""; flex: 1; border-top: 1px solid var(--rule); }
.rq-conclusion.rq-ipm-goal { grid-template-columns: minmax(0, 1fr); }
.rq-conclusion[data-change].rq-ipm-goal { border-left-color: #5c9870; }
.rq-captured [data-change] { background: #edf5ef; border-left-color: #5c9870; }
.rq-hyp[data-change] .rq-hyp-names::before { content: "↻ "; color: #38664d; font-size: 0.7rem; }
.rq-hyp[data-change=added] .rq-hyp-names::before { content: "+ "; }
.rq-conclusion[data-change] .rq-turnstile::after { content: " ↻"; color: #38664d; }
.rq-unparsed { font: 0.8rem/1.6 var(--mono-font); white-space: pre-wrap; overflow-wrap: anywhere; }
.rq-other-goal { border-top: 1px solid var(--rule); padding: 0.25rem 0; }
.rq-other-goal > summary { cursor: pointer; color: var(--muted); font-size: 0.8rem; }
.rq-complete { color: #38664d; padding: 0.3rem 0; margin: 0; }
.rq-incomplete { color: var(--muted); }
.rq-before { padding-bottom: 0.4rem; border-bottom: 1px dashed var(--rule); }
.rq-before::before { content: "Before"; display: block; margin-bottom: 0.15rem; font-size: 0.75rem; color: var(--muted); }
.rq-before [data-change] { background: transparent; border-left-color: transparent; }
.rq-script { border-top: 1px solid var(--rule); margin-top: 0.4rem; padding-top: 0.3rem; }
.rq-script > summary { font-size: 0.75rem; color: var(--muted); cursor: pointer; }
@container (max-width: 45rem) {
  .rq-walk { grid-template-columns: minmax(0, 1fr); gap: 0.4rem; }
  .rq-dialog .rq-walk { display: flex; flex-direction: column; align-items: stretch; }
  .rq-dialog .rq-timeline { display: contents; }
  .rq-dialog .rq-timeline .rq-focus { display: contents; }
  .rq-dialog .rq-step-link {
    padding-left: calc(0.25rem + min(var(--depth), 6) * 0.45rem);
    background-image: repeating-linear-gradient(90deg, var(--rule) 0 1px, transparent 1px 0.45rem);
    background-size: calc(min(var(--depth), 6) * 0.45rem) 100%;
    background-position: 0.25rem 0;
    background-repeat: no-repeat;
  }
  /* On a phone the selected state follows its tactic in one scroll flow. */
  .rq-dialog .rq-explorer { display: block; overflow-y: auto; overscroll-behavior: contain; }
  .rq-dialog .rq-timeline { overflow: visible; }
  .rq-dialog .rq-states { overflow: visible; padding: 0.3rem 0; border-block: 1px solid var(--rule); }
  .rq-dialog .rq-script[open] { max-height: none; overflow: visible; }
  .rq-dialog .rq-proof-controls { order: 1; flex-basis: 100%; }
  .rq-proof-controls .rq-compare { margin-left: 0; }
}
@media (max-width: 48rem) {
  .rq-dialog { width: 100vw; height: 100dvh; border: 0; padding-inline: 0.6rem; }
}

/* Modules: their sentences under a rule. */
section.rq-module { margin: 1.2rem 0; scroll-margin-top: 3rem; }
.rq-module-body { margin-left: 0.5em; padding-left: 0.9em; border-left: 2px solid var(--rule); }
.rq-notation .notation .op { color: var(--ink); }
.rq-mods { color: var(--muted); font-size: 0.82em; }
pre.rq-raw { font-size: 0.82rem; position: relative; }

/* Rocq in documents. */
.rq-fence { margin: 0.5rem 0 0.9rem 1rem; }

.rq-nav li.type > a { color: var(--ty); }
.rq-nav li.lemma > a, .rq-nav li.axiom > a { color: var(--lem); }

/* Rows become readable cards, not squeezed columns with lost comments.
   Variables let the container default and the explicit choice share a layout. */
:is(table.rq-ctors, table.rq-fields, table.rq-comparison) { display: var(--rq-table, table); }
:is(table.rq-ctors, table.rq-fields, table.rq-comparison) tbody { display: var(--rq-body, table-row-group); }
:is(table.rq-ctors, table.rq-fields, table.rq-comparison) tr {
  display: var(--rq-row, table-row); grid-template-columns: minmax(0, 1fr);
  padding-block: var(--rq-row-pad, 0); border-bottom: var(--rq-row-border, 0);
}
:is(table.rq-ctors, table.rq-fields, table.rq-comparison) td {
  display: var(--rq-cell, table-cell); min-width: 0;
  white-space: var(--rq-space, normal); border-bottom: 0;
}
table.rq-ctors td.bar { display: var(--rq-bar, table-cell); }
:is(table.rq-ctors, table.rq-fields) td:is(.ctor, .field-name) { white-space: var(--rq-space, nowrap); }
:is(table.rq-ctors, table.rq-fields) td:is(.ctor-aside, .field-aside) { max-width: none; color: var(--muted); }
.rq-comparison td::before {
  content: attr(data-label); display: var(--rq-label-display, none); font-size: 0.7rem;
  color: var(--muted); text-transform: uppercase; letter-spacing: 0.04em; margin-top: 0.3rem;
}
.rq-comparison thead { display: var(--rq-thead, table-header-group); }
.rq-comparison td:first-child { min-width: 0; white-space: var(--rq-space, normal); }
.dterm .prose .rq-comparison code.rq :is(.c, .args, .arg) { white-space: normal; }

@container (max-width: 40rem) {
  :is(table.rq-ctors, table.rq-fields) {
    --rq-table: block; --rq-body: block; --rq-row: grid; --rq-cell: block;
    --rq-bar: none; --rq-space: normal; --rq-row-pad: 0.5rem;
    --rq-row-border: 1px solid var(--rule);
  }
  :is(.dterm-rocq, code.rq) .binder { white-space: normal; }
  .dterm-rocq .cases.stack { padding-inline: 0.2em; margin-left: 0; border: 0; border-radius: 0; }
  .dterm-rocq .cases.match.stack { grid-template-columns: 0.8em minmax(0, 1fr); }
  .rq-app > .app-args, .rq-fun > .fun-body, .rq-let > .let-value { padding-left: 0.4em; margin-left: 0; }
  .rules, .rq-thm > .rule { margin-left: 0.4em; }
}
@container (max-width: 55rem) {
  .rq-comparison {
    --rq-table: block; --rq-body: block; --rq-row: grid; --rq-cell: block;
    --rq-space: normal; --rq-row-pad: 0.7rem; --rq-row-border: 1px solid var(--rule);
    --rq-thead: none; --rq-label-display: block;
  }
}
html[data-case-layout="stack"] :is(table.rq-ctors, table.rq-fields, table.rq-comparison) {
  --rq-table: block; --rq-body: block; --rq-row: grid; --rq-cell: block;
  --rq-bar: none; --rq-space: normal; --rq-row-pad: 0.5rem;
  --rq-row-border: 1px solid var(--rule); --rq-thead: none; --rq-label-display: block;
}
html[data-case-layout="table"] :is(table.rq-ctors, table.rq-fields, table.rq-comparison) {
  --rq-table: block; --rq-body: table-row-group; --rq-row: table-row; --rq-cell: table-cell;
  --rq-bar: table-cell; --rq-space: nowrap; --rq-row-pad: 0;
  --rq-row-border: 0; --rq-thead: table-header-group; --rq-label-display: none;
  overflow-x: auto;
}
html[data-case-layout="table"] .tactic { display: block; max-width: 100%; overflow-x: auto; }
@media (max-width: 700px) {
  body:has(.rq-layout) .status nav.crumbs { min-width: 0; white-space: normal; overflow: visible; }
  body:has(.rq-layout) .status .crumb.current { display: inline-block; max-width: 100%; overflow-wrap: anywhere; vertical-align: top; }
  body:has(.rq-layout, .rq-index) .status .status-right { display: none; }
  /* The formal campaign compares Rocq with Prolog terms in the same
     paragraphs. Both need to wrap on a phone. */
  .guide:has(.rq-layout) .prose code.term :is(.c, .args, .arg, .binder) { white-space: normal; }
  /* Source-page prose can contain long names too (Runtime's toolchain
     revision, for example); it must not widen the proof reading surface. */
  .dterm-rocq :is(.prose, .rq-files) code.term { overflow-wrap: anywhere; }
  .dterm-rocq :is(.prose, .rq-files) code.term :is(.c, .args, .arg, .binder) { white-space: normal; }
  .rq-comparison td:first-child { min-width: 0; }
  .rule { display: grid; }
  /* A rule's ∀ line breaks where it must, like a goal: a binder's type
     such as option (contract (LK.callback_world payload)) has no space
     to break at. */
  .rule-vars { overflow-wrap: anywhere; }
}