diff options
Diffstat (limited to 'plugins/ssrsearch')
| -rw-r--r-- | plugins/ssrsearch/g_search.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
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 |