Stop using revert dependent

See https://github.com/coq/coq/pull/17669. `revert dependent` is an
alias for `generalize dependent` and is going away soon.

stdpp/fin.v

@@ -65,9 +65,9 @@ Ltac inv_fin i :=
   | fin ?n =>
     match eval hnf in n with
     | 0 =>
-      revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
+      generalize dependent i; match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
     | S ?n =>
-      revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
+      generalize dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
     end
   end.
 

stdpp/vector.v

@@ -88,9 +88,9 @@ Ltac inv_vec v :=
   match eval hnf in T with
   | vec _ ?n =>
     match eval hnf in n with
-    | 0 => revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
+    | 0 => generalize dependent v; match goal with |- ∀ v, @?P v => apply (vec_0_inv P) end
     | S ?n =>
-      revert dependent v; match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end;
+      generalize dependent v; match goal with |- ∀ v, @?P v => apply (vec_S_inv P) end;
       (* Try going on recursively. *)
       try (let x := fresh "x" in intros x v; inv_vec v; revert x)
     end