aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
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
2017-08-16Merge PR #943: Reference Manual: minor wording improvementsMaxime Dénès
2017-08-16Merge PR #940: Replace jarring use of "Remark" with "Note"Maxime Dénès
2017-08-16Merge PR #934: Fix some coq-tex errors in the reference manual.Maxime Dénès
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-08-02Rewording the introductionEnrico Tassi
2017-08-02Rephrasing a couple of sentences in a more factual way.Hugo Herbelin
2017-08-02Rephrasing the introduction in a more factual and up-to-date way.Hugo Herbelin
2017-08-02Port ssr manual to Coq's latex/hevea styleEnrico Tassi
2017-08-02Makefile.doc: implement serve-refman-8080 targetEnrico Tassi
2017-08-02Update Setoid.texlarsr
2017-08-02Typo in the documentation of cumulativityAmin Timany
2017-08-01Unbreak RecTutorial.vGaëtan Gilbert
2017-08-01Remove old doc/rt files.Gaëtan Gilbert
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-08-01Improve style slightlySam Pablo Kuper
2017-08-01Merge PR #933: Fix documentation of Hint Mode (bug #4911).Maxime Dénès
2017-08-01Merge PR #932: Fix shuffled documentation.Maxime Dénès
2017-08-01Merge PR #929: Add missing paragraph to introductionMaxime Dénès
2017-08-01Merge PR #925: Document Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:26:27 +0000