aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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.
2018-07-12[ci] Remove warning jobs in favor of default `-warn-error yes`Emilio Jesus Gallego Arias
As discussed in #6930, we remove the warnings jobs and instead do require the developers to submit a clean build.
2018-07-12Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gaëtan Gilbert
2018-07-12Tactic deprecation machineryMaxime Dénès
We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
2018-07-11[ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Emilio Jesus Gallego Arias
- We update the OCaml version used in the base CI image. - Windows / OSX image building is also updated to use newer OCaml. - We also update Dune to 1.0.0.
2018-07-11Merge PR #7998: [coqpp] Move to its own directory.Pierre-Marie Pédrot
2018-07-11Merge PR #8035: Fix #8033: Tactic assert-suceeds has a typo in its name in ↵Théo Zimmermann
the manual
2018-07-11Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integersPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 14:10:54 +0000