Merge PR #17889: Fixes #17817: refer to actual chosen extraction lang…

…uage in extraction error messages Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
coq · Aug 1, 2023 · 3974f34 · 3974f34
2 parents 677b524 + 5389409
commit 3974f34
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/...13-misc/17889-master+fix17817-extraction-prop-elim-error-not-ocaml-specific.rst b/...13-misc/17889-master+fix17817-extraction-prop-elim-error-not-ocaml-specific.rst
@@ -0,0 +1,7 @@
+- **Fixed:**
+  In the error message about extraction of sort-polymorphic
+  singleton inductive types, do not specifically refer to OCaml as
+  other languages are also concerned
+  (`#17889 <https://github.com/coq/coq/pull/17889>`_,
+  fixes `#17817 <https://github.com/coq/coq/issues/17817>`_,
+  by Hugo Herbelin).
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
@@ -410,7 +410,7 @@ let error_singleton_become_prop id og =
        str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++
        str "This happens when a sort-polymorphic singleton inductive type\n" ++
        str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
-       str "The Ocaml extraction cannot handle this situation yet.\n" ++
+       str "Extraction cannot handle this situation yet.\n" ++
        str "Instead, use a sort-monomorphic type such as (True /\\ True)\n" ++
        str "or extract to Haskell.")