Update README.md

README.md

@@ -8,30 +8,30 @@ to the `examples` folder.
 second on my computer - slow enough to be noticed, but not too slow.
 
 ## Examples
-* [`cbv_vs_Qed`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/cbv_vs_Qed.v)
-  : in some situations, `cbv` without options is more efficient than `Qed`.
-* [`forgotten_strategy`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/forgotten_strategy.v)
-  : Coq may not track the details of the proving strategy and this can lead
+* [`cbv_vs_Qed`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/cbv_vs_Qed.v):
+  in some situations, `cbv` without options is more efficient than `Qed`.
+* [`forgotten_strategy`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/forgotten_strategy.v):
+  Coq may not track the details of the proving strategy and this can lead
   to performance issues at `Qed` time.
-* [`frustration`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/frustration.v)
-  : there's no way simple way of unfolding a fixpoint only once.
-* [`manual_check_slower_than_Qed`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/manual_check_slower_than_Qed.v)
-  : `Qed` is more efficient at typechecking than `Definition` or `Check`.
-* [`memoization`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/memoization.v)
-  : `vm_compute` memoizes constants.
-* [`names`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/names.v)
-  : non-breaking spaces can be used in identifiers for some reason.
-* [`name_checking_halfway`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/name_checking_halfway.v)
-  : Coq's typechecking procedure seems to be split into at least three phases.
+* [`frustration`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/frustration.v):
+there's no way simple way of unfolding a fixpoint only once.
+* [`manual_check_slower_than_Qed`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/manual_check_slower_than_Qed.v):
+  `Qed` is more efficient at typechecking than `Definition` or `Check`.
+* [`memoization`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/memoization.v):
+  `vm_compute` memoizes constants.
+* [`names`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/names.v):
+  non-breaking spaces can be used in identifiers for some reason.
+* [`name_checking_halfway`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/name_checking_halfway.v):
+  Coq's typechecking procedure seems to be split into at least three phases.
   Phase 1 and phase 3 look redundant to me, and the check of the validity of the
-  name of the element being defined occurs at phase 2.
-* [`nonlinear_computation`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/nonlinear_computation.v)
-  : twice as much work can take more than twice as much time.
-* [`now_is_not_reflexivity`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/now_is_not_reflexivity.v)
-  : easy tends to be slower than reflexivity, and `now` uses `easy`.
-* [`simpl_vs_cbn`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/simpl_vs_cbn.v)
-  : `simpl` doesn't like deep nestings.
-* [`time_lies`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/time_lies.v)
-  : take `Time`'s output with a pinch of salt.
-* [`unfolding_and_traces`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/unfolding_and_traces.v)
-  : `unfold` and `intro` don't commute.
+  identifier occurs at phase 2.
+* [`nonlinear_computation`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/nonlinear_computation.v):
+  twice as much work can take more than twice as much time.
+* [`now_is_not_reflexivity`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/now_is_not_reflexivity.v):
+  `easy` tends to be slower than `reflexivity`, and `now` uses `easy`.
+* [`simpl_vs_cbn`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/simpl_vs_cbn.v):
+  `simpl` doesn't like deep nestings.
+* [`time_lies`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/time_lies.v):
+  take `Time`'s output with a pinch of salt.
+* [`unfolding_and_traces`](https://gitlab.epfl.ch/baty1/fourriere/-/blob/master/examples/unfolding_and_traces.v):
+  `unfold` and `intro` don't commute.