summaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Correct some spelling errorsmasterBenjamin Barenblat2018-07-22
* Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' o...Théo Zimmermann2018-07-22
|\
| * Solved problems with snippets giving errors in chapter 'Detailed examples of ...Zeimer2018-07-21
| * Rewrote examples about permutations, logic and type isomorphisms: changed the...Zeimer2018-07-21
| * Improvements for the chapter 'Detailed examples of tactics' of the Reference ...Zeimer2018-07-21
|/
* Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' an...Théo Zimmermann2018-07-21
|\
* \ Merge PR #8086: Improved chapter 'The tactic language' of the Reference Manual.Théo Zimmermann2018-07-21
|\ \
| * | Small improvements suggested in comments to PR #8086.Zeimer2018-07-20
| * | Improved chapter 'The tactic language' of the Reference Manual.Zeimer2018-07-20
|/ /
| * Added :undocumented: and :cmd: as suggested in comments for PR #8072.Zeimer2018-07-20
| * Fixed many spelling and grammar errors in the chapters 'Vernacular commands',...Zeimer2018-07-20
|/
* Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Enrico Tassi2018-07-20
|\
* \ Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.Enrico Tassi2018-07-20
|\ \
* \ \ Merge PR #8070: Fixed some typos and grammar errors from section 'The languag...Théo Zimmermann2018-07-20
|\ \ \
| * | | Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' o...Zeimer2018-07-19
| * | | Fixed some typos and grammar errors from section 'The language' of the Refere...Zeimer2018-07-19
|/ / /
* | | Merge PR #7941: Extend QuestionMark to produce a better error message in case...Pierre-Marie Pédrot2018-07-19
|\ \ \
| | * | Remove declare_object for SsrHave NoTCResolution.Maxime Dénès2018-07-19
| |/ / |/| |
* | | Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi2018-07-18
|\ \ \
* \ \ \ Merge PR #7897: Remove fourier pluginEnrico Tassi2018-07-18
|\ \ \ \
* \ \ \ \ Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence`Enrico Tassi2018-07-18
|\ \ \ \ \
* \ \ \ \ \ Merge PR #8060: Remove useless libobject in proof_usingEnrico Tassi2018-07-18
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #8055: Fast accumulator check in native compilationMaxime Dénès2018-07-17
|\ \ \ \ \ \ \
| | | | * | | | Remove fourier pluginMaxime Dénès2018-07-17
| |_|_|/ / / / |/| | | | | |
| | | | | * | change into QuestionMark defaultSiddharth Bhat2018-07-17
| | | | | * | Add overlay for Coq-Equations for QuestionMark.Siddharth Bhat2018-07-17
| | | | | * | Change QuestionMark for better record field missing error message.Siddharth Bhat2018-07-17
| |_|_|_|/ / |/| | | | |
* | | | | | Merge PR #8069: Only check overlay extensions on git-tracked filesGaëtan Gilbert2018-07-16
|\ \ \ \ \ \
| * | | | | | Only check overlay extensions on git-tracked filesJason Gross2018-07-16
|/ / / / / /
* | | | | | Merge PR #8023: Introduce a team of code owners for the CI system.Maxime Dénès2018-07-16
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #8066: [ltac] Remove unused functions.Pierre-Marie Pédrot2018-07-16
|\ \ \ \ \ \ \
| | | | | * | | [build] Build Coq and plugins with `-strict-sequence`Emilio Jesus Gallego Arias2018-07-14
| |_|_|_|/ / / |/| | | | | |
| * | | | | | [ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias2018-07-14
|/ / / / / /
* | | | | | Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of th...Théo Zimmermann2018-07-13
|\ \ \ \ \ \
| | | | * | | Remove useless libobject in proof_usingMaxime Dénès2018-07-13
* | | | | | | Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib.Emilio Jesus Gallego Arias2018-07-13
|\ \ \ \ \ \ \
| * | | | | | | Make -warn-error fail on warnings emitted by coqc on stdlib.Maxime Dénès2018-07-13
|/ / / / / / /
| | | * | | | Generate type-specific code for is_accu in native compilation of fixpoints.Pierre-Marie Pédrot2018-07-13
| | | * | | | Store the {struct} inductive type in native fixpoint AST.Pierre-Marie Pédrot2018-07-13
| | | * | | | Pass a proper environment to Nativelambda.lambda_of_constr.Pierre-Marie Pédrot2018-07-13
| * | | | | | Fixed typos, wording and grammar errors in the Preamble of the Reference Manu...Zeimer2018-07-12
* | | | | | | Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes`Gaëtan Gilbert2018-07-12
|\ \ \ \ \ \ \ | |_|_|/ / / / |/| | | | | |
* | | | | | | Merge PR #7907: Tactic deprecation machineryPierre-Marie Pédrot2018-07-12
|\ \ \ \ \ \ \ | |_|/ / / / / |/| | | | | |
| | | | | * | [dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias2018-07-12
| |_|_|_|/ / |/| | | | |
* | | | | | Merge PR #8051: Clean-up user-overlays folder.Emilio Jesus Gallego Arias2018-07-12
|\ \ \ \ \ \
| * | | | | | Clean-up user-overlays folder.Théo Zimmermann2018-07-12
| | |_|_|/ / | |/| | | |
| | | * | | [warnings] Disable warning 58 "no cmx file was found in path"Emilio Jesus Gallego Arias2018-07-12
| | | * | | [warnings] Disable warning 59 [assignment to a non-mutable value] to make fla...Emilio Jesus Gallego Arias2018-07-12
| | | * | | [ci] Remove warning jobs in favor of default `-warn-error yes`Emilio Jesus Gallego Arias2018-07-12
| |_|/ / / |/| | | |
* | | | | Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gaëtan Gilbert2018-07-12
|\ \ \ \ \ | |/ / / / |/| | | |