diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:07 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:57:07 +0100 |
| commit | 3690e568a36f8b418ec9c253a3188403f53021ba (patch) | |
| tree | 78e428676766abab6fc49dec53c95c3fc89a5d22 /CHANGES | |
| parent | fcdddca6124eec4d34e1f57a39aadbd2b082ffcf (diff) | |
| parent | 1ed79649c0435336c98a1d8b89e1ccc36b8107cc (diff) | |
Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language command
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -39,6 +39,8 @@ Vernacular Commands - The deprecated Coercion Local, Open Local Scope, Notation Local syntax was removed. Use Local as a prefix instead. +- For the Extraction Language command, "OCaml" is spelled correctly. + The older "Ocaml" is still accepted, but deprecated. Universes |