diff options
| author | Pierre-Marie Pédrot | 2016-06-27 20:47:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-27 20:47:43 +0200 |
| commit | 663a8647bbc32e11243091de80f9953ed5fb7eff (patch) | |
| tree | 7fba0a308daee7586221f752e233dd8fa9c8f5f5 /doc | |
| parent | d4725f692a5f202ca4c5d6341b586b0e377f6973 (diff) | |
| parent | a7ea32fbf3829d1ce39ce9cc24b71791727090c5 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'doc')
| -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 9da23b54ed..01dbcfb1cb 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. |