Deeplim inverses some equalities when sections are involved

[thomas-lamiaux]

I found a weird behavior with depelim. In the code below, depelim keeps inverting the equality

Section Foo.
  Context (x y : vec nat 2).

Definition foo (H : x = y) : x = y.
  depelim H.
  depelim H.
  depelim H.

but with this code, the equality gets deleted

Definition foo (x y : vec nat 2) (H : x = y) : x = y.
  depelim H.

[thomas-lamiaux]

It actually behaves weird for section variables all together. Compare

Section Foo.
  Context (A : Type).
  Context (a b : A).
  Context (x y : vec A 2).
  Context (z : vec A 3).

Goal (vcons a (vcons a x) = vcons a (vcons b y)) -> a = b /\ x = y.
  intros H. depelim H. now split.
Qed.

Goal (vcons a x = z) -> vtail z = x.
  intros H. depelim H. subst. simp vtail. easy.
Qed.

End Foo.

and

Section Foo.
  Context (A : Type).
  Context (a b : A).

Goal forall (x y : vec A 2), (vcons a (vcons a x) = vcons a (vcons b y)) -> a = b /\ x = y.
  intros x y H. depelim H. now split.
Qed.

Goal forall ( x : vec A 2) z, (vcons a x = z) -> vtail z = x.
  intros x z H. depelim H. simp vtail. reflexivity.
Qed.