the new representation of branches in 8.14 breaks old code, esp. 'remember' tactic

[formalize]

Description of the problem

In previous versions branches were mere functions and could be targeted by 'remember', 'replace', 'rewrite' etc. but not anymore in 8.14.

For example:

Lemma foo (T: Type) (a: option T) (y: T):
  match a with
  | Some x => x
  | None => y
  end = y.
remember (fun (x: T) => x) as f.

in 8.13 that produces:

Some x => f x

but in 8.14 it no longer changes anything.

I'm using remember on branches all the time and this change breaks a lot of code, and I don't know what to replace it with because 'rewrite' does not always dare to descend into difficult-to-destruct dependently typed matches whereas 'remember' just did the job. I'll have to stay on 8.13 for now.

[herbelin]

because 'rewrite' does not always dare to descend into difficult-to-destruct dependently typed matches whereas 'remember' just did the job

Could you give a full use case so that we understand better your need? (In any case, the old behavior could be emulated.)

[formalize]

Ok, here's a bigger example:

Require Import Arith List.

Definition nth_cert {A : Type} (l : list A) (n : nat) (Ok : n < length l)
: { x : A | In x l }
:= match nth_error l n as z return _ = z -> _ with
   | Some x => fun E => exist _ x (nth_error_In l n E) 
   | None => fun E => match lt_not_le _ _ Ok (proj1 (nth_error_None l n) E) with end
   end eq_refl.

Lemma nth_cert_ok {A : Type} (l : list A) (n : nat) (Ok : n < length l):
  nth_error l n = Some (proj1_sig (nth_cert l n Ok)).
Proof.
unfold nth_cert.
(* destruct (nth_error l n). (* that doesn't work *) *)
remember (fun x E => exist (fun x0 : A => In x0 l) x (nth_error_In l n E))
  as some_branch.
remember (fun E => match lt_not_le n (length l) Ok (proj1 (nth_error_None l n) E)
                   with end) as none_branch.
assert (SomeBranchOk: forall a E,
                        Some a = Some (proj1_sig (some_branch a E))).
{ intros. now subst. }
assert (NoneBranchOk: forall E, None = Some (proj1_sig (none_branch E))).
{ intros. exfalso. exact (lt_not_le n (length l) Ok (proj1 (nth_error_None l n) E)). }
clear Heqsome_branch Heqnone_branch.
destruct (nth_error l n); [apply SomeBranchOk | apply NoneBranchOk].
Qed.