diff options
| author | Matej Kosik | 2016-06-20 15:08:11 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-06-20 15:10:39 +0200 |
| commit | 0fa8b96c243e0915477866b094735ecaaaac6ef6 (patch) | |
| tree | 9e9b4d046a087b1dbf9684611338bf29a5fdd6b7 | |
| parent | c064fb933a16dc25b8172a1a2e758f538ee7285e (diff) | |
Reference Manual / Extraction: the original example command no longer works with recent Coq
| -rw-r--r-- | doc/refman/Extraction.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index a963662f64..ee156b652c 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -448,7 +448,7 @@ let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y)) happens when there is a quantification over types inside the type of a constructor; for example: \begin{verbatim} -Inductive anything : Set := dummy : forall A:Set, A -> anything. +Inductive anything : Type := dummy : forall A:Set, A -> anything. \end{verbatim} which corresponds to the definition of an ML dynamic type. |