../ compilation.rstFixed indentation of enumerated list.11 years ago documenting.rstDocs for new record syntax11 years ago elaborator-reflection.rstMerge pull request #2408 from mjgpy3/metavariable_to_hole_docs11 years ago erasure.rstHeading normalisation, and reST usage fixes.12 years ago ffi.rstDocs for new record syntax11 years ago ide-protocol.rstParser-driven highlighting of quasiquoted regions11 years ago index.rstFix missing index contents11 years ago language-extensions.rstUpdates11 years ago language-features.rstPruning and deduplication of content in the reference documentation.11 years ago misc.rstPruning and deduplication of content in the reference documentation.11 years ago packages.rstUpdates11 years ago repl.rstReplace "metavariable" with "hole"11 years ago semantic-highlighting.rstFix typos in semantic highlighting docs11 years ago syntax-guide.rstFixed syntax for commands and some words11 years ago tactics.rstReplace "metavariable" with "hole"11 years ago uniqueness-types.rstHeading normalisation, and reST usage fixes.12 years ago