Merge branch 'deprecated-revert-dependent' into 'master'

Stop using revert dependent

See merge request iris/stdpp!481

stdpp/fin.v

@@ -65,9 +65,11 @@ 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,12 @@ 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