aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2017-11-06Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Samuel Gruetter
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
2017-10-27Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631Maxime Dénès
2017-10-25Rename \Tree to \NatTreeJohannes Kloos
2017-10-25Put newlines at the end of files.Gaëtan Gilbert
2017-10-24Fix #5763: Strictly positive example is out of order.jkloos
2017-10-24Fix #4846Johannes Kloos
2017-10-24Fix #5413: [unfold ... in] not documentedJohannes Kloos
2017-10-24Documentation: Add various basic constructs to the index.Johannes Kloos
2017-10-24Fix part of 'Hard to find documentation for `(...) and `{...} #5631'Johannes Kloos
2017-10-11Remove GeoProof support.Maxime Dénès
2017-10-10Merge PR #1116: Updating citing Coq in FAQ.Maxime Dénès
2017-10-10Updating citing Coq in FAQ.Hugo Herbelin
2017-10-06Fix copyright info in reference manual.Théo Zimmermann
2017-10-05Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Maxime Dénès
2017-10-03Merge PR #1080: Remove some unused parts of the reference manual.Maxime Dénès
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-22Remove some unused parts of the reference manual.Guillaume Melquiond
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-09-13Reference manual: A few words about the file system constraints for -Q/-R.Hugo Herbelin
2017-09-11Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Maxime Dénès
2017-09-11Merge PR #1035: Fix the introduction of SSR refman chapter.Maxime Dénès
2017-09-11Merge PR #1014: Add option index entry for NativeCompute ProfilingMaxime Dénès
2017-09-11Merge PR #1004: Document primitive projections in more detailMaxime Dénès
2017-09-08Fix Typo in Doc for `Set Parsing Explicit`staffehn
2017-09-08Fix the introduction of SSR refman chapter.Théo Zimmermann
2017-09-032 Typos in 'Add Parametric Morphism' Documentationstaffehn
2017-09-01add option index entry for NativeCompute ProfilingPaul Steckler
2017-08-31Document primitive projections in more detailMatthieu Sozeau
2017-08-31RefMan-ssr: fix warningMatthieu Sozeau
2017-08-31Merge PR #993: Credits for version 8.7Maxime Dénès
2017-08-31Credits for version 8.7Matthieu Sozeau
2017-08-31Merge PR #958: coq_makefile: build/use .cma for packed plugins tooMaxime Dénès
2017-08-29coq_makefile: improve documentationEnrico Tassi
2017-08-29Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Maxime Dénès
2017-08-29Merge PR #988: Fix obsolete description of real numerals.Maxime Dénès
2017-08-29Merge PR #819: Cleanup old thingsMaxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-23Update coypright dates on documentationMatthieu Sozeau
2017-08-22Fix obsolete description of real numerals.Guillaume Melquiond
2017-08-18use OCaml temp_file, instead of our own versionPaul Steckler
2017-08-18Merge PR #973: Adding documentation for Printing Focused option.Maxime Dénès
2017-08-17Add native compute profiling, BZ#5170Paul Steckler
2017-08-17Merge PR #974: Change section caption, improve some wordingMaxime Dénès
2017-08-17Document anonymous universes (PR #544).Gaëtan Gilbert
2017-08-17Adding documentation for Printing Focused option.Pierre Courtieu
2017-08-16mention that tactic is the identity or gives errorPaul Steckler
2017-08-16change section caption, improve some wordingPaul Steckler
2017-08-16Merge PR #831: Port ssreflect user manual to Coq's latex/hevea styleMaxime Dénès
2017-08-16Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:41:01 +0000