aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2018-07-11Merge PR #8002: make-both-single-timing-files: fix --sort-by=diffJason Gross
2018-07-11Merge PR #7898: Remove camlp4 remainsEmilio Jesus Gallego Arias
2018-07-11[coqpp] Move to its own directory.Emilio Jesus Gallego Arias
Coqpp has nothing to do with `grammar`, we thus place it in its own directory, which will prove convenient in more modular build systems. Note that we add `coqpp` to the list of global includes, we could have indeed added some extra rules, but IMHO not worth it as hopefully proper containment will be soon checked by Dune.
2018-07-11Merge PR #7984: Compile `coqpp` inside the `bin/` folder and make it ↵Emilio Jesus Gallego Arias
available after installation
2018-07-11Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it.Emilio Jesus Gallego Arias
2018-07-10Export a function to apply toplevel tactic values in Tacinterp.Pierre-Marie Pédrot
This is a function that keeps beeing asked or reimplemented. It doesn't hurt adding it to the Ltac API.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:34:10 +0000