diff options
Diffstat (limited to 'doc/refman/CanonicalStructures.tex')
| -rw-r--r-- | doc/refman/CanonicalStructures.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index 7b3bdcf4a9..b1c278cede 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -305,8 +305,10 @@ canonical structures. We need some infrastructure for that. -\begin{coq_example} +\begin{coq_example*} Require Import Strings.String. +\end{coq_example*} +\begin{coq_example} Module infrastructure. Inductive phantom {T : Type} (t : T) : Type := Phantom. Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := |