diff options
| author | Gaëtan Gilbert | 2020-07-03 15:15:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-03 15:15:20 +0200 |
| commit | cf388fdb679adb88a7e8b3122f65377552d2fb94 (patch) | |
| tree | b852fd1e116ff72748210a11bc95298453ac2e4d /plugins | |
| parent | 33581635d3ad525e1d5c2fb2587be345a7e77009 (diff) | |
| parent | 53e19f76624b7a18792af799e970e9478f8e90a9 (diff) | |
Merge PR #12523: Fix #11121: Simultaneous definition of term and notation in custom gr…
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: herbelin
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 8 | ||||
| -rw-r--r-- | plugins/ssrsearch/g_search.mlg | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 162013c556..1ed632f03f 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -859,7 +859,7 @@ let glob_cpattern gs p = | k, (v, Some t), _ as orig -> if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else match t.CAst.v with - | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ in _ )"), ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> @@ -867,11 +867,11 @@ let glob_cpattern gs p = | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ as _ )"), ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> + | CNotation(_,(InConstrEntry,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; 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 |