Why is this `apply`

not doing the usual reflection thing, and is just a no-op? I must be missing something....

```
From Coq Require Import Unicode.Utf8.
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Lemma foo b : b = false.
Proof.
Set Printing All.
apply/negPf.
```

Googling leads to https://github.com/coq/coq/issues/10391 — I'm not sure what's going on, but the first example with move /negPf strongly implies that's related

It seems https://github.com/math-comp/math-comp/issues/284#issuecomment-463204494 lists the actual answer, although I don't yet follow.

@Pierre Roux Will do then, with pleasure :)

Pierre Jouvelot has marked this topic as unresolved.

Last updated: Jul 23 2024 at 21:01 UTC