From 11e1bf77cef9f3ecf901b30381119bd1e06de52e Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe@bedrocksystems.com>
Date: Fri, 16 Feb 2024 16:19:04 +0100
Subject: [PATCH] Support for prefix attribute.

---
 apps/derive/elpi/derive.elpi         | 4 +++-
 apps/derive/elpi/derive_synterp.elpi | 4 +++-
 apps/derive/theories/derive.v        | 1 +
 3 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/apps/derive/elpi/derive.elpi b/apps/derive/elpi/derive.elpi
index 640302711..7f9e7cdf0 100644
--- a/apps/derive/elpi/derive.elpi
+++ b/apps/derive/elpi/derive.elpi
@@ -107,7 +107,9 @@ main T P CL :- main1 T P CL.
 
 pred main1 i:gref, i:bool, o:list prop.
 main1 T P CL :-
-  if (P = tt) (Prefix is {coq.gref->id T} ^ "_") (Prefix = ""),
+  if (get-option "prefix" PFX)
+     (Prefix = PFX)
+     (if (P = tt) (Prefix is {coq.gref->id T} ^ "_") (Prefix = "")),
   std.findall (derivation T Prefix _ _) L,
   if (L = [])
      (coq.error "no derivation found, did you Import derive.std?")
diff --git a/apps/derive/elpi/derive_synterp.elpi b/apps/derive/elpi/derive_synterp.elpi
index 1b56d0ac7..e75d57155 100644
--- a/apps/derive/elpi/derive_synterp.elpi
+++ b/apps/derive/elpi/derive_synterp.elpi
@@ -60,7 +60,9 @@ main T P :- main1 T P.
 
 pred main1 i:string, i:bool.
 main1 T P :-
-  if (P = tt) (Prefix is T ^ "_") (Prefix = ""),
+  if (get-option "prefix" PFX)
+     (Prefix = PFX)
+     (if (P = tt) (Prefix is T ^ "_") (Prefix = "")),
   std.findall (derivation T Prefix _) L,
   std.map L (x\r\ x = derivation _ _ r) DL,
   toposort DL SortedDL,
diff --git a/apps/derive/theories/derive.v b/apps/derive/theories/derive.v
index 2bda372da..051e35ef7 100644
--- a/apps/derive/theories/derive.v
+++ b/apps/derive/theories/derive.v
@@ -69,6 +69,7 @@ Elpi Db derive.with_attributes lp:{{
       att "verbose" bool,
       att "only" attmap,
       att "recursive" bool,
+      att "prefix" string,
     ] Opts, !,
     Opts => P.
 }}.