diff options
| author | Hugo Herbelin | 2015-01-24 22:25:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-24 22:27:57 +0100 |
| commit | 27aec3933031ec5e87738965c25ffa51863c9400 (patch) | |
| tree | 5eb5e3704ee7357dba5f079e6ed766cbaa9ed9cb | |
| parent | bb37153d90de103dabd02285d11b3c39e3e4f89c (diff) | |
Doc: Fixing some compilation problems with chapter Canonical
Structures. Text mode + a "Require Import" in a module which provokes
suspect warnings "Exception Not_found".
| -rw-r--r-- | doc/refman/CanonicalStructures.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index 28a6f69032..c8e36197ca 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -306,8 +306,8 @@ canonical structures. We need some infrastructure for that. \begin{coq_example} +Require Import Strings.String. Module infrastructure. - Require Import Strings.String. Inductive phantom {T : Type} (t : T) : Type := Phantom. Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 -> phantom t2. Definition id {T} {t : T} (x : phantom t) := x. @@ -318,8 +318,8 @@ Module infrastructure. End infrastructure. \end{coq_example} -To explain the notation $[find v | t1 \textasciitilde t2]$ lets pick one -of its instances: $[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]$. +To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one +of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}. It should be read as: ``find a class e such that its objects have type T or fail with message "T is not an EQ.type"''. |