From 8c113b5af0a861318c0185ff4f4dc1614fa166b4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 26 Jul 2023 16:06:49 +0200 Subject: [PATCH 1/2] Fixes #17817: extraction error message refers to actual language of extraction. --- plugins/extraction/table.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2fd3c9734721..6c84e88274d7 100644 --- 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.") From 53894097bfcb97380198acd5f72a8672196811c2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 26 Jul 2023 16:12:30 +0200 Subject: [PATCH 2/2] Adding changelog for #17889 --- ...17817-extraction-prop-elim-error-not-ocaml-specific.rst | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog/13-misc/17889-master+fix17817-extraction-prop-elim-error-not-ocaml-specific.rst diff --git a/doc/changelog/13-misc/17889-master+fix17817-extraction-prop-elim-error-not-ocaml-specific.rst b/doc/changelog/13-misc/17889-master+fix17817-extraction-prop-elim-error-not-ocaml-specific.rst new file mode 100644 index 000000000000..9443e07b886a --- /dev/null +++ b/doc/changelog/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 `_, + fixes `#17817 `_, + by Hugo Herbelin).