From c0d07d59605ba92e2657bb890e9ac23cdc7f857c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Sun, 12 Jan 2025 14:02:03 +0100
Subject: [PATCH] Fix missing match cases for prim strings in notation.ml

Fix #20020
---
 interp/notation.ml              |  3 +++
 test-suite/output/bug_20020.out |  2 ++
 test-suite/output/bug_20020.v   | 11 +++++++++++
 3 files changed, 16 insertions(+)
 create mode 100644 test-suite/output/bug_20020.out
 create mode 100644 test-suite/output/bug_20020.v

diff --git a/interp/notation.ml b/interp/notation.ml
index 3bc21494ef6a..c543a4574dfa 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -553,6 +553,7 @@ let rec check_glob env sigma g c = match DAst.get g, Constr.kind c with
      sigma, mkApp (c, Array.of_list cl)
   | Glob_term.GInt i, Constr.Int i' when Uint63.equal i i' -> sigma, mkInt i
   | Glob_term.GFloat f, Constr.Float f' when Float64.equal f f' -> sigma, mkFloat f
+  | Glob_term.GString s, Constr.String s' when Pstring.equal s s' -> sigma, mkString s
   | Glob_term.GArray (_,t,def,ty), Constr.Array (_,t',def',ty') ->
      let sigma,u = Evd.fresh_array_instance env sigma in
      let sigma,def = check_glob env sigma def def' in
@@ -613,6 +614,7 @@ let rec constr_of_glob to_post post env sigma g = match DAst.get g with
       end
   | Glob_term.GInt i -> sigma, mkInt i
   | Glob_term.GFloat f -> sigma, mkFloat f
+  | Glob_term.GString s -> sigma, mkString s
   | Glob_term.GArray (_,t,def,ty) ->
       let sigma, u' = Evd.fresh_array_instance env sigma in
       let sigma, def' = constr_of_glob to_post post env sigma def in
@@ -641,6 +643,7 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
   | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None))
   | Int i -> DAst.make ?loc (Glob_term.GInt i)
   | Float f -> DAst.make ?loc (Glob_term.GFloat f)
+  | String s -> DAst.make ?loc (Glob_term.GString s)
   | Array (u,t,def,ty) ->
       let def' = glob_of_constr token_kind ?loc env sigma def
       and t' = Array.map (glob_of_constr token_kind ?loc env sigma) t
diff --git a/test-suite/output/bug_20020.out b/test-suite/output/bug_20020.out
new file mode 100644
index 000000000000..62932ad0f341
--- /dev/null
+++ b/test-suite/output/bug_20020.out
@@ -0,0 +1,2 @@
+"bla"%ts
+     : t
diff --git a/test-suite/output/bug_20020.v b/test-suite/output/bug_20020.v
new file mode 100644
index 000000000000..2b4a53c75edb
--- /dev/null
+++ b/test-suite/output/bug_20020.v
@@ -0,0 +1,11 @@
+Require PrimString.
+
+Declare Scope t_scope.
+Delimit Scope t_scope with ts.
+
+Import PrimString.
+Inductive t := v : string -> t.
+Definition parse : string -> t := v.
+Definition print : t -> string := fun x => match x with v s => s end.
+String Notation t parse print : t_scope.
+Check v "bla".                (* string notation not used: [v "bla"] *)