From 53e19f76624b7a18792af799e970e9478f8e90a9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 16 Jun 2020 17:09:40 +0200
Subject: Fix #11121: Simultaneous definition of term and notation in custom
 grammar

---
 plugins/ssrsearch/g_search.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssrsearch')

diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index f5cbf2005b..5e002e09cc 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -59,7 +59,7 @@ let interp_search_notation ?loc tag okey =
          (Bytes.set s' i' '_'; loop (j + 1) (i' + 2))
       else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in
     loop 0 1 in
-  let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in
+  let trim_ntn (pntn, m) = (InConstrEntry,Bytes.sub_string pntn 1 (max 0 m)) in
   let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in
   let pr_and_list pr = function
     | [x] -> pr x
-- 
cgit v1.2.3