diff options
| -rw-r--r-- | doc/changelog/05-tactic-language/12541-fix12228.rst | 6 | ||||
| -rw-r--r-- | tactics/redexpr.ml | 14 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12228.v | 4 |
3 files changed, 22 insertions, 2 deletions
diff --git a/doc/changelog/05-tactic-language/12541-fix12228.rst b/doc/changelog/05-tactic-language/12541-fix12228.rst new file mode 100644 index 0000000000..286760e008 --- /dev/null +++ b/doc/changelog/05-tactic-language/12541-fix12228.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Excluding occurrences was causing an anomaly in tactics + (e.g., :g:`pattern _ at L` where :g:`L` is :g:`-2`). + (`#12541 <https://github.com/coq/coq/pull/12541>`_, + fixes `#12228 <https://github.com/coq/coq/issues/12228>`_, + by Pierre Roux). diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index e000ddce74..c463c06cd5 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -188,8 +188,18 @@ let out_arg = function | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") | Locus.ArgArg x -> x +let out_occurrences occs = + let occs = Locusops.occurrences_map (List.map out_arg) occs in + match occs with + | Locus.OnlyOccurrences (n::_ as nl) when n < 0 -> + Locus.AllOccurrencesBut (List.map abs nl) + | Locus.OnlyOccurrences nl when List.exists (fun n -> n < 0) nl -> + CErrors.user_err Pp.(str "Illegal negative occurrence number.") + | Locus.OnlyOccurrences _ | Locus.AllOccurrencesBut _ | Locus.NoOccurrences + | Locus.AllOccurrences | Locus.AtLeastOneOccurrence -> occs + let out_with_occurrences (occs,c) = - (Locusops.occurrences_map (List.map out_arg) occs, c) + (out_occurrences occs, c) let e_red f env evm c = evm, f env evm c @@ -199,7 +209,7 @@ let head_style = false (* Turn to true to have a semantics where simpl let contextualize f g = function | Some (occs,c) -> - let l = Locusops.occurrences_map (List.map out_arg) occs in + let l = out_occurrences occs in let b,c,h = match c with | Inl r -> true,PRef (global_of_evaluable_reference r),f | Inr c -> false,c,f in diff --git a/test-suite/bugs/closed/bug_12228.v b/test-suite/bugs/closed/bug_12228.v new file mode 100644 index 0000000000..a874fa0570 --- /dev/null +++ b/test-suite/bugs/closed/bug_12228.v @@ -0,0 +1,4 @@ +Tactic Notation "mark" constr(P) "at" integer_list(L) := pattern P at L. +Goal 0 = 0. +mark 0 at -2. +Abort. |