Sampsa Kiiskinen

As if living with the rooster was not hard enough already, some proofs in the standard library start with both `Next Obligation` and `Proof` and thus manifest this issue. The...

I seem to keep bumping my head onto issues that have already been considered; sorry about that. In this case (and even in general), it would be helpful to know...

I am sympathetic to your pleas of innocence, but since this is the reality we have to live in, I would like to know whether the appropriate course of action...

While writing the report for coq/coq#14132, I noticed that `Program` allows defining `h` by using the first presentation, while the equations plugin fails to generate enough hypotheses. Why do _with...

Using that pattern in _with clauses_ indeed works, but also introduces definitions like `h_unfold_clause_1`, which need to be unfolded by hand. This would be a good situation to make use...

While `match` has such a feature, it does not seem to be recognized by `Equations`. ``` Program Fixpoint base_fix (a : N) {measure a lt} : N := match a...

Thanks for the clues. While it is true that it would probably be wise to only highlight the cursor in the active buffer, this is not necessarily the case with...

This problem also plagues module subtype relations, as seen in Coq's own `theories/Arith/PeanoNat.v`. ```coq Module Nat

The `apply_funelim` tactic should be mentioned in the reference manual.

Also, lemmas and variables, whose names start with `exists`, are highlighted as if they were quantifiers. ```coq From Coq Require Import Lists.List. Search existsb. ``` ```coq existsb_app: forall [A :...