Add changelog for #17902

coq · Jul 31, 2023 · ac165b4 · ac165b4
1 parent b9a867b
commit ac165b4
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/...s/17902-master+fix11237-constructor-parameters-in-prim-notation-for-pattern.rst b/...s/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 <https://github.com/coq/coq/pull/17902>`_,
+  fixes `#11237 <https://github.com/coq/coq/issues/11237>`_,
+  by Hugo Herbelin).
diff --git 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.