From ac165b467c19923062fc7ed1d17d2c9d2535be57 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 28 Jul 2023 15:19:23 +0200 Subject: [PATCH] Add changelog for #17902 --- ...7-constructor-parameters-in-prim-notation-for-pattern.rst | 5 +++++ test-suite/output/StringSyntaxPrimitive.v | 1 + 2 files changed, 6 insertions(+) create mode 100644 doc/changelog/03-notations/17902-master+fix11237-constructor-parameters-in-prim-notation-for-pattern.rst diff --git a/doc/changelog/03-notations/17902-master+fix11237-constructor-parameters-in-prim-notation-for-pattern.rst b/doc/changelog/03-notations/17902-master+fix11237-constructor-parameters-in-prim-notation-for-pattern.rst new file mode 100644 index 000000000000..837a936bd191 --- /dev/null +++ b/doc/changelog/03-notations/17902-master+fix11237-constructor-parameters-in-prim-notation-for-pattern.rst @@ -0,0 +1,5 @@ +- **Fixed:** + support constructors with parameters in number or string notations for patterns + (`#17902 `_, + fixes `#11237 `_, + by Hugo Herbelin). diff --git a/test-suite/output/StringSyntaxPrimitive.v b/test-suite/output/StringSyntaxPrimitive.v index f5fe657f881d..8dbca8da4c24 100644 --- a/test-suite/output/StringSyntaxPrimitive.v +++ b/test-suite/output/StringSyntaxPrimitive.v @@ -142,6 +142,7 @@ Module Bug11237. Inductive bytes := wrap_bytes { unwrap_bytes : list byte }. +Declare Scope bytes_scope. Delimit Scope bytes_scope with bytes. Bind Scope bytes_scope with bytes. String Notation bytes wrap_bytes unwrap_bytes : bytes_scope.