The float_let tactic breaks with Coq 8.10.2

[lastland]

The float_let tactic (defined in

hs-to-coq/examples/ghc/theories/GhcTactics.v

Lines 44 to 60 in d4b61b8

	(** This tactic finds a [let x := rhs in body] anywhere in the goal,
	and moves it into the context, without zeta-reducing it. *)
	Ltac find_let e k :=
	lazymatch e with
	| let x := ?rhs in ?body => k x rhs body
	| ?e1 ?e2 =>
	find_let e1 ltac:(fun x rhs body => k x rhs uconstr:(body e2)) ||
	find_let e2 ltac:(fun x rhs body => k x rhs uconstr:(e1 body))
	| _ => fail
	end.
	Ltac float_let :=
	lazymatch goal with |- ?goal =>
	find_let goal ltac:(fun x rhs body =>
	let goal' := uconstr:(let x := rhs in body) in
	(change goal'; intro) || fail 1000 "Failed to change to" goal'
	)
	end.

) is broken under Coq 8.10.2. I think it's a bug of Coq itself, and I have opened an issue here: coq/coq#11389

As before the issue gets fixed, I have a temporary workaround that works with our existing proofs: 74e83ea#diff-4c03f5269c19d75442f5862b0de92ef1

I'm recording this here, to keep track of the issue, and so that anyone who runs into the problem with this tactic knows what happened.