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: Oct 13 2024 at 01:02 UTC