From c3914be79f963687915b1eb26566c1c58e90b8ef Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 25 Jan 2024 21:21:03 +0100
Subject: [PATCH] fix opam dep

---
 coq-elpi.opam                     | 2 +-
 src/coq_elpi_builtins_synterp.ml  | 7 +++++--
 src/coq_elpi_builtins_synterp.mli | 2 +-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/coq-elpi.opam b/coq-elpi.opam
index 89f963769..118585cd0 100644
--- a/coq-elpi.opam
+++ b/coq-elpi.opam
@@ -15,7 +15,7 @@ install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
   "ocaml" {>= "4.09.0" }
   "stdlib-shims"
-  "elpi" {>= "1.18.1" & < "1.19.0~"}
+  "elpi" {>= "1.18.2" & < "1.19.0~"}
   "coq" {>= "8.19" & < "8.20~" }
   "dot-merlin-reader" {with-dev}
   "ocaml-lsp-server" {with-dev}
diff --git a/src/coq_elpi_builtins_synterp.ml b/src/coq_elpi_builtins_synterp.ml
index 6ea44f15d..5f1f187ad 100644
--- a/src/coq_elpi_builtins_synterp.ml
+++ b/src/coq_elpi_builtins_synterp.ml
@@ -53,7 +53,7 @@ let scope = let open Conv in let open API.AlgebraicData in declare {
 
 let grafting = let open Conv in let open API.AlgebraicData in declare {
   ty = TyName "grafting";
-  doc = "Specify if the clause has to be grafted before or after a named clause";
+  doc = "Specify if the clause has to be grafted before, grafted after or replace a named clause";
   pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
   constructors = [
     K("before","",A(id,N),
@@ -62,10 +62,13 @@ let grafting = let open Conv in let open API.AlgebraicData in declare {
     K("after","",A(id,N),
         B (fun x -> (`After,x)),
         M (fun ~ok ~ko -> function (`After,x) -> ok x | _ -> ko ()));
+    K("replace","",A(id,N),
+      B (fun x -> (`Replace,x)),
+      M (fun ~ok ~ko -> function (`Replace,x) -> ok x | _ -> ko ()));
   ]
 } |> CConv.(!<)
 
-type clause = string option * ([ `After | `Before ] * string) option * API.Data.term
+type clause = string option * ([ `After | `Before | `Replace ] * string) option * API.Data.term
 
 let clause = let open Conv in let open API.AlgebraicData in declare {
   ty = TyName "clause";
diff --git a/src/coq_elpi_builtins_synterp.mli b/src/coq_elpi_builtins_synterp.mli
index 0d94104b0..b6ab7bd80 100644
--- a/src/coq_elpi_builtins_synterp.mli
+++ b/src/coq_elpi_builtins_synterp.mli
@@ -52,7 +52,7 @@ val set_accumulate_to_db_synterp :
 val prop : Data.term Conversion.t
 val id : string Conversion.t
 
-type clause = string option * ([ `After | `Before ] * string) option * Data.term
+type clause = string option * ([ `After | `Before | `Replace ] * string) option * Data.term
 
 val clause : clause Conversion.t