Dune already supports chrome://tracing/ style profiling Coq and libraries builds at the file level with the --trace-file option. We should integrate this with per-sentence timing so profiles display per-sentence data.

There is now a type circle in UniMath.SyntheticHomotopyTheory.Circle2. It would be great to define pi_1 of a pointed type, and to show that pi_1(circle, pt) \simeq Z.

Counter examples today show information in tables to invalidate the equivalence, but does not show the result of the queries that makes evident that difference. It would be great if you could add that.

When long lines are broken down, some indentation is usually applied by Format. The amount of indentation is stored in the Vbox/Hbox/Hovbox but is currently ignored by jsCoq.

Proof General (v8.10+β2):

<img width="990" src="https:

• Document the new option coq-errormsg-as-failure added in #238 (in CHANGES and PG doc)
• Also, document somewhere (e.g. in the Wiki) the new behavior of pg: async regarding retraction.
  Sources: ProofGeneral/PG#238 (comment), ProofGeneral/PG#238 (comment)
  See also: <https://github.com/ProofGeneral/PG/p

I could not find in the reviewing checklist a note on how to merge.
In particular if the PR has overlays, one has to merge them.

Hey folks,

I use emacs 26.2 with the development version of spacemacs.
The autocompletion works fine but two doc buffers are opened when the documentation of some element is shown. One doc buffer is the original one generated from
company-coq and the other is the company-quickhelp pos-tip window which should subsume
the doc buffer.

I

Just saying QuickChick uses arguments to customize execution doesn't give the user much guidance about how they could pass an Args record to QC if they needed to. (For example, they might want a different value for the max number of successes in different sections, so defining it as a global constant doesn't work...)

Also there is something very confusing.
As far as I understand:

Require Import Program.
From Equations Require Import Equations.

will use dependent induction of Program.

But

Require Import Program.
From Equations Require Import Equations.
Require Import Equations.Prop.DepElim.

will use dependent induction of Equations.
:-)

I personally don't care for custom formatting styles, but @maximedenes is very particular. To speed up development, and never have to worry about whitespace again, we should decide on a .prettierrc and format the codebase accordingly. Docs are here.

See #24

Re: siegebell/vscoq#91 (comment)

It's possible to overwrite the styles for the ProofView window by running the Coq: Customize proof-view styling command, which is a great customization feature! It'd be helpful to highlight this feature somewhere in the README and/or the wiki docs.

Any thoughts on where this should live if we want to do this?