aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-11Merge PR #12815: [micromega] Fix bug#12790Vincent Laporte
Reviewed-by: vbgl
2020-08-11Merge PR #12814: [zify] fix for bug#12791Vincent Laporte
Reviewed-by: vbgl
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot
2020-08-10[micromega] Fix bug#12790Frédéric Besson
zify used to generate many syntactic positivity constraints when translating a goal from nat to Z. For instance, to state that the product of 2 integers is positive. Instead, lia performs an interval analysis that is more semantic. The bug was that the interval analysis was performed after the elimination of equations. The current workaround is to perform interval analysis before and after eliminating equations. bla
2020-08-10[zify] fix for bug#12791Frédéric Besson
The elimination of let bindings is performing a convertibility check in order to deal with type aliases.
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-08Merge PR #12796: [default.nix] Propagate dependency on num following #12604.Vincent Laporte
Reviewed-by: vbgl
2020-08-07[default.nix] Propagate dependency on num following #12604.Théo Zimmermann
Since this PR, ocamlfind looks for num when building plugins. To avoid requiring all plugins to add a new, irrelevant, dependency, we propagate it. This solution imitates what was decided for nixpkgs in NixOS/nixpkgs#94230. Fix coq-community/aac-tactics#61.
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM ↵coqbot
environment variable Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-08-06Merge PR #12782: Trying to rephrase complex sentences to make them easier to ↵coqbot
read. Reviewed-by: jfehrle Ack-by: Mbodin Ack-by: corwin-of-amber
2020-08-06Trying to rephrase complex sentences to make them easier to read.Martin Bodin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-08-05Merge PR #12724: CI metacoq: make .merlincoqbot
Reviewed-by: Zimmi48
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-08-04Merge PR #12706: Mention coqbot minimize feature in issue template.coqbot
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: jtcoolen
2020-08-04Mention coqbot minimize feature in issue template.Julien Coolen
This allows coqbot to reply back with a minimized version of some code reproducing a bug, using the coq-bug-minimizer program from Jason Gross. See https://github.com/JasonGross/coq-tools#coq-bug-minimizer.
2020-08-03Merge PR #12772: coqdoc: Fix the “details” environmentLi-yao Xia
Reviewed-by: Lysxia
2020-07-30Merge PR #12767: Fix do in ssreflect-proof-language.rstcoqbot
Reviewed-by: Zimmi48
2020-07-29coqdoc: Fix the “details” environmentThomas Letan
The change introduced by 41a1d66 has broken the feature prior to its initial release. We attempt to fix the issue, and add a comment to warn feature developers in order to avoid facing the same issue again.
2020-07-29Fix do in ssreflect-proof-language.rstYusuke Matsushita
The tactics do in SSReflect uses `? @mult` rather than `? @num`.
2020-07-28Merge PR #12754: Fixes #12752: applying symbol escaping in coqdoc indexLi-yao Xia
Reviewed-by: Lysxia
2020-07-27Merge PR #12729: Faster algorithm to compute algebraic universe mapping in ↵Gaëtan Gilbert
minimization. Reviewed-by: SkySkimmer
2020-07-26Merge PR #12726: Clarify Global.env usage in ppvernacPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-26Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque ↵Pierre-Marie Pédrot
Defined constants Reviewed-by: ppedrot
2020-07-25Faster algorithm to compute algebraic universe mapping in mimization.Pierre-Marie Pédrot
Instead of crawling a map in O(n) we preserve a backwards map at the same time. This inefficiency was observed in coq-performance-tests/n_polymorphic_universes.v.
2020-07-24Adding change log for #12754.Hugo Herbelin
2020-07-24Fixes #12752 (applying symbol escaping in index produced by coqdoc).Hugo Herbelin
This is to avoid collision with the syntax of the host output language.
2020-07-24Merge PR #12747: Fix coqdoc bad bulleting from incorrect space countEmilio Jesus Gallego Arias
Reviewed-by: Lysxia Reviewed-by: ejgallego Ack-by: ppedrot
2020-07-24CI metacoq: make .merlinGaëtan Gilbert
For convenience
2020-07-24Fix coqdoc bad bulleting from incorrect space countGaëtan Gilbert
Fix #12742
2020-07-23Merge PR #12739: [changelog] Fix hanging changelog entry for 8.12 betaThéo Zimmermann
Ack-by: Zimmi48
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Fix hanging file extension.Emilio Jesus Gallego Arias
2020-07-23Merge PR #12734: [changelog] Latest changes backported to 8.12 branch.Théo Zimmermann
Reviewed-by: Zimmi48
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-23Merge PR #12678: Tweak the warning for arbitrary term hints.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
Helps with #12566
2020-07-23Merge PR #12672: Fix failing macOS build.Gaëtan Gilbert
Ack-by: JasonGross Reviewed-by: SkySkimmer
2020-07-23Ignore installation failure during call to brew.Théo Zimmermann
Note that all the packages that we request are correctly installed and the observed failure is independent (related to ruby which is not a direct nor indirect dependency, only a dependency of brew itself). The generated CoqIDE package has been tested and works correctly (with no missing icon).
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: silene
2020-07-23Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a ↵Théo Zimmermann
qualid in tactic notations Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-07-22Merge PR #12715: Add Coqtail to CIGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-22Clarify Global.env usage in ppvernacGaëtan Gilbert
2020-07-22Merge PR #12664: Turn various anomalies into regular errors in primitive ↵Pierre-Marie Pédrot
declaration path Reviewed-by: ppedrot
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
No need to store the case_info, all the data is reconstructible from the context. Furthermore, this reconstruction is performed in a context where we already access the environment, so performance is not at stake. Hopefully this will also reduce the number of globally allocated VM values, since the switch representation now only depends on the shape of the inductive type.
2020-07-21Merge PR #12714: [declare] Remove some dead code in declare_mutual_definitionGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-21Add Coqtail to CIwhonore
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-21Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a ↵Emilio Jesus Gallego Arias
generic printing format in anticipation of further not-only-parsing uses of the notation Reviewed-by: ppedrot
2020-07-20[declare] Remove some dead code in declare_mutual_definitionEmilio Jesus Gallego Arias
This is a leftover after the unification of constant information, `kind` is now correctly set by the single caller of `Obls.add_mutual_definitions`.
2020-07-20Merge PR #12712: CI: deploy make-built stdlib docEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:16:39 +0000