From e32901fe344e608a79b6a1e4cf5ad3376c14a21e Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 15 Jul 2024 11:17:50 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19216

---
 Changelog.md             |  5 +++++
 src/coq_elpi_builtins.ml | 40 ++++++++++++++++++++++++++++++++++++++--
 2 files changed, 43 insertions(+), 2 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index 6da18cfcb..13b1a80c4 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,3 +1,8 @@
+# unreleased
+
+### API
+- New `coq.arguments.reset-simplification`
+
 # [2.2.2] - 15/07/2024
 
 Requires Elpi 1.19.2 and Coq 8.19 or Coq 8.20.
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index c56612510..3d7734901 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -1331,6 +1331,40 @@ let coq_header_builtins =
 |};
   ]
 
+[%%if coq = "8.19" || coq = "8.20" ]
+let compat_reduction_behavior_set ~local gref strategy =
+  Reductionops.ReductionBehaviour.set ~local gref strategy
+[%%else]
+let compat_reduction_behavior_set ~local gref strategy =
+  Reductionops.ReductionBehaviour.set ~local gref (Some strategy)
+[%%endif]
+
+[%%if coq = "8.19" || coq = "8.20" ]
+let compat_reset_simplification = []
+[%%else]
+let compat_reset_simplification =
+  let open API.BuiltIn in
+  let open Pred in
+  let open Notation in
+  let open CConv in
+  let pp ~depth = P.term depth in
+  [MLCode(Pred("coq.arguments.reset-simplification",
+    In(gref,"GR",
+    Full(global,
+{|resets the behavior of the simplification tactics.
+Also resets the ! and / modifiers for the Arguments command.
+Supported attributes:
+- @global! (default: false)|})),
+  (fun gref ~depth { options } _ -> grab_global_env "coq.arguments.reset-simplification" (fun state ->
+     match gref with
+     | ConstRef gref ->
+       let local = options.local <> Some false in
+       Reductionops.ReductionBehaviour.set ~local gref None;
+       state, (), []
+     | _ -> err Pp.(str "reset-simplification must be called on constant")))),
+  DocAbove)]
+[%%endif]
+
 let coq_misc_builtins =
   let open API.BuiltIn in
   let open Pred in
@@ -3083,10 +3117,12 @@ Supported attributes:
      match gref with
      | ConstRef gref ->
        let local = options.local <> Some false in
-       Reductionops.ReductionBehaviour.set ~local gref strategy;
+       compat_reduction_behavior_set ~local gref strategy;
        state, (), []
      | _ -> err Pp.(str "set-simplification must be called on constant")))),
-  DocAbove);
+  DocAbove)
+
+  ] @ compat_reset_simplification @ [
 
   MLCode(Pred("coq.locate-abbreviation",
     In(id, "Name",