more 'forall' -> 'universal' quantification

Author: simongregersen

exercises/later.v

@@ -185,12 +185,12 @@ Proof.
     The tactic for Löb induction, [iLöb], requires us to specify the
     name of the induction hypothesis, which we here call ["IH"].
     Optionally, it can also universally quantify over any of our variables
-    before performing induction. We here forall quantify [x] as it changes for
-    every recursive call.
+    before performing induction. We here universally quantify over [x] as it
+    changes for every recursive call.
   *)
   iLöb as "IH" forall (x).
   (**
-    [iLöb] automatically introduces the forall quantified variables in
+    [iLöb] automatically introduces the universally quantified variables in
     the goal, so we can proceed to execute the function.
   *)
   wp_rec.

exercises/linked_lists.v

@@ -53,9 +53,9 @@ Lemma inc_spec (l : val) (xs : list Z) :
   {{{ RET #(); isList l ((λ x, #(x + 1)) <$> xs)}}}.
 Proof.
   (**
-    The proof proceeds by structural induction in [xs]. As [l] changes
-    in each iteration, we must forall quantify it to strengthen the
-    induction hypothesis.
+    The proof proceeds by structural induction in [xs]. As [l] changes in each
+    iteration, we must universally quantify over it to strengthen the induction
+    hypothesis.
   *)
   revert l.
   induction xs as [|x xs' IH]; simpl.

theories/later.v

@@ -188,12 +188,12 @@ Proof.
     The tactic for Löb induction, [iLöb], requires us to specify the
     name of the induction hypothesis, which we here call ["IH"].
     Optionally, it can also universally quantify over any of our variables
-    before performing induction. We here forall quantify [x] as it changes for
-    every recursive call.
+    before performing induction. We here universally quantify over [x] as it
+    changes for every recursive call.
   *)
   iLöb as "IH" forall (x).
   (**
-    [iLöb] automatically introduces the forall quantified variables in
+    [iLöb] automatically introduces the universally quantified variables in
     the goal, so we can proceed to execute the function.
   *)
   wp_rec.

theories/linked_lists.v

@@ -53,9 +53,9 @@ Lemma inc_spec (l : val) (xs : list Z) :
   {{{ RET #(); isList l ((λ x, #(x + 1)) <$> xs)}}}.
 Proof.
   (**
-    The proof proceeds by structural induction in [xs]. As [l] changes
-    in each iteration, we must forall quantify it to strengthen the
-    induction hypothesis.
+    The proof proceeds by structural induction in [xs]. As [l] changes in each
+    iteration, we must universally quantify over it to strengthen the induction
+    hypothesis.
   *)
   revert l.
   induction xs as [|x xs' IH]; simpl.