Doc: Overfull lines in chapter on Canonical Structures.

1 files changed, 8 insertions, 4 deletions

diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index c8e36197c..7b3bdcf4a 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -309,11 +309,15 @@ We need some infrastructure for that.
 Require Import Strings.String.
 Module infrastructure.
   Inductive phantom {T : Type} (t : T) : Type := Phantom.
-  Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2.
+  Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) :=
+    phantom t1 -> phantom t2.
   Definition id {T} {t : T} (x : phantom t) := x.
-  Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) (at level 50, v ident, only parsing).
-  Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) (at level 50, v ident, only parsing).
-  Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error'  :  t  :  s").
+  Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
+    (at level 50, v ident, only parsing).
+  Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
+    (at level 50, v ident, only parsing).
+  Notation "'Error : t : s" := (unify _ t (Some s))
+    (at level 50, format "''Error'  :  t  :  s").
   Open Scope string_scope.
 End infrastructure.
 \end{coq_example}