aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-07-24Merge PR #8000: Fix #7854: Native compilation + flambda trigger SEGFAULT.Maxime Dénès
2018-07-24Merge PR #6597: Binary, Octal, and Hex conversions between [positive], [Z], ↵Hugo Herbelin
[N], [nat] and [string]
2018-07-22Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' ↵Théo Zimmermann
of the Reference Manual.
2018-07-21Solved problems with snippets giving errors in chapter 'Detailed examples of ↵Zeimer
tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged.
2018-07-21Rewrote examples about permutations, logic and type isomorphisms: changed ↵Zeimer
the formatting and renamed the tactics to match modern naming conventions.
2018-07-21Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵Zeimer
Manual.
2018-07-21Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵Théo Zimmermann
and 'Tactics' of the Reference Manual.
2018-07-21Merge PR #8086: Improved chapter 'The tactic language' of the Reference Manual.Théo Zimmermann
2018-07-20Small improvements suggested in comments to PR #8086.Zeimer
2018-07-20Improved chapter 'The tactic language' of the Reference Manual.Zeimer
2018-07-20Added :undocumented: and :cmd: as suggested in comments for PR #8072.Zeimer
2018-07-20Fixed many spelling and grammar errors in the chapters 'Vernacular ↵Zeimer
commands', 'Proof handling' and 'Tactics' of the Reference Manual. Fixed some more serious errors related to tactics functional induction, unfold, hnf and red. Added some error messages and remarks for tactics btauto, rtauto and red.
2018-07-20Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Enrico Tassi
2018-07-20Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.Enrico Tassi
2018-07-20Merge PR #8070: Fixed some typos and grammar errors from section 'The ↵Théo Zimmermann
language' of the Reference Manual.
2018-07-19Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵Zeimer
of the Reference Manual.
2018-07-19Fixed some typos and grammar errors from section 'The language' of the ↵Zeimer
Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes.
2018-07-19Merge PR #7941: Extend QuestionMark to produce a better error message in ↵Pierre-Marie Pédrot
case of missing record field
2018-07-19Remove declare_object for SsrHave NoTCResolution.Maxime Dénès
IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like `Global Set SsrHave NoTCResolution`. I don't think it is needed (just let the user write the desired locality), but if it is, the right way of doing it is to let clients of Goptions specify a default locality.
2018-07-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
2018-07-18Merge PR #7897: Remove fourier pluginEnrico Tassi
2018-07-18Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence`Enrico Tassi
2018-07-18Merge PR #8060: Remove useless libobject in proof_usingEnrico Tassi
2018-07-17Merge PR #8055: Fast accumulator check in native compilationMaxime Dénès
2018-07-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-07-17change into QuestionMark defaultSiddharth Bhat
2018-07-17Add overlay for Coq-Equations for QuestionMark.Siddharth Bhat
The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this.
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields.
2018-07-16Merge PR #8069: Only check overlay extensions on git-tracked filesGaëtan Gilbert
2018-07-16bin,oct,hex conversions positive,Z,N,nat<->stringJason Gross
2018-07-16Only check overlay extensions on git-tracked filesJason Gross
This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git.
2018-07-16Merge PR #8023: Introduce a team of code owners for the CI system.Maxime Dénès
2018-07-16Merge PR #8066: [ltac] Remove unused functions.Pierre-Marie Pédrot
2018-07-14[build] Build Coq and plugins with `-strict-sequence`Emilio Jesus Gallego Arias
Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins.
2018-07-14[ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias
Catched by compiling the ml files from ml4.
2018-07-13Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵Théo Zimmermann
the Reference Manual (Introduction, Credits).
2018-07-13Remove useless libobject in proof_usingMaxime Dénès
2018-07-13Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib.Emilio Jesus Gallego Arias
2018-07-13Make -warn-error fail on warnings emitted by coqc on stdlib.Maxime Dénès
We turn all Coq warnings that are on by default into errors.
2018-07-13Generate type-specific code for is_accu in native compilation of fixpoints.Pierre-Marie Pédrot
This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument.
2018-07-13Store the {struct} inductive type in native fixpoint AST.Pierre-Marie Pédrot
2018-07-13Pass a proper environment to Nativelambda.lambda_of_constr.Pierre-Marie Pédrot
No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions.
2018-07-12Fixed typos, wording and grammar errors in the Preamble of the Reference ↵Zeimer
Manual (Introduction, Credits).
2018-07-12Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes`Gaëtan Gilbert
2018-07-12Merge PR #7907: Tactic deprecation machineryPierre-Marie Pédrot
2018-07-12[dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias
For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
2018-07-12Merge PR #8051: Clean-up user-overlays folder.Emilio Jesus Gallego Arias
2018-07-12Clean-up user-overlays folder.Théo Zimmermann
2018-07-12[warnings] Disable warning 58 "no cmx file was found in path"Emilio Jesus Gallego Arias
See https://github.com/ocaml/num/issues/9
2018-07-12[warnings] Disable warning 59 [assignment to a non-mutable value] to make ↵Emilio Jesus Gallego Arias
flambda happy. See issue #8043. Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like an OCaml bug.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:31:44 +0000