diff options
| author | Pierre-Marie Pédrot | 2020-06-29 15:37:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:37:14 +0200 |
| commit | 1221b56974398d96a7df833e7b32d4b7bc044338 (patch) | |
| tree | 5782e7012612f5f85bb4c7417b691b17992b1b54 | |
| parent | a039e78c821ba6a0da5d3364b98491707eab8add (diff) | |
| parent | d958feb5f30255d3b9ca84bf5be89c299ddb8a5f (diff) | |
Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_list
Reviewed-by: ppedrot
| -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. |