diff options
| author | Pierre-Marie Pédrot | 2015-12-08 18:12:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-08 18:12:27 +0100 |
| commit | e70165079e8defe490a568ece20a7029e4c1626e (patch) | |
| tree | 7e8ad97cbe6e06251fae9cc2da48acc8ab36d303 /plugins/extraction | |
| parent | 071a458681254716a83b1802d5b6a30edda37892 (diff) | |
| parent | 19ea51a4b7f7debbe5bdeb2b2689cddadd9876f4 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6ae519ef60..1112c3b890 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -734,7 +734,7 @@ and extract_cst_app env mle mlt kn u args = if la >= ls then (* Enough args, cleanup already done in [mla], we only add the - additionnal dummy if needed. *) + additional dummy if needed. *) put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla)) else (* Partially applied function with some logical arg missing. @@ -748,7 +748,7 @@ and extract_cst_app env mle mlt kn u args = (*s Extraction of an inductive constructor applied to arguments. *) (* \begin{itemize} - \item In ML, contructor arguments are uncurryfied. + \item In ML, constructor arguments are uncurryfied. \item We managed to suppress logical parts inside inductive definitions, but they must appears outside (for partial applications for instance) \item We also suppressed all Coq parameters to the inductives, since |