diff options
| author | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
| commit | dd84c113a154742dff86328ebc758097e9aac8eb (patch) | |
| tree | 67795fb720516f564d074d55d9e2aa90e3d4e7f2 /plugins/ssr | |
| parent | 231f679965745a4d7677166e8d5f62a38ebde4e7 (diff) | |
| parent | 569ad299a8092778611fcc8ae2842151c4b276db (diff) | |
Merge PR #8115: Support for custom entries in notations (take 2, feature part)
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 8ce0316f53..989a6c5bf1 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -217,8 +217,8 @@ 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) = Bytes.sub_string pntn 1 (max 0 m) in - let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in + let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,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 | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x @@ -293,7 +293,7 @@ let interp_search_notation ?loc tag okey = let scs' = List.remove (=) sc !scs in let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in Feedback.msg_warning (hov 4 w) - else if String.string_contains ~where:ntn ~what:" .. " then + else if String.string_contains ~where:(snd ntn) ~what:" .. " then err (pr_ntn ntn ++ str " is an n-ary notation"); let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in let rec sub () = function |