From f1f334f7f7473fd9f480ee3ce3119df8fe52c401 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 28 Jan 2025 11:03:24 +0100
Subject: [PATCH 1/3] Fix a typo

---
 apps/derive/elpi/param2.elpi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/apps/derive/elpi/param2.elpi b/apps/derive/elpi/param2.elpi
index 3a1ae4221..22c28388a 100644
--- a/apps/derive/elpi/param2.elpi
+++ b/apps/derive/elpi/param2.elpi
@@ -174,7 +174,7 @@ dispatch (const GR as C) Suffix Clauses :- do! [
   C1 = (param Term Term (global (const TermR)) :- !),
   coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "param:fail") C1),
   C2 = (paramR Term Term (global (const TermR)) :- !),
-  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "paramR:fail") C1),
+  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "paramR:fail") C2),
   coq.elpi.accumulate _ "derive.param2.db" (clause _ _ (param-done C)),
   Clauses = [param-done C, C1, C2]
 ].

From abf6d7c55082bf32640b5089a8b69e6277c8ff8a Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 28 Jan 2025 11:02:54 +0100
Subject: [PATCH 2/3] Add derive.param2.register

---
 apps/derive/elpi/param2.elpi         |  9 +++++++++
 apps/derive/tests/test_param2.v      |  9 +++++++++
 apps/derive/theories/derive/param2.v | 11 +++++++++++
 3 files changed, 29 insertions(+)

diff --git a/apps/derive/elpi/param2.elpi b/apps/derive/elpi/param2.elpi
index 22c28388a..2894ab1e8 100644
--- a/apps/derive/elpi/param2.elpi
+++ b/apps/derive/elpi/param2.elpi
@@ -222,6 +222,15 @@ pred main i:gref, i:string, o:list prop.
 main T _ Clauses :-
   dispatch T "_R" Clauses.
 
+pred main_register i:gref, i:gref.
+main_register I R :-
+  GI = global I, GR = global R,
+  C1 = (param GI GI GR :- !),
+  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "param:fail") C1),
+  C2 = (paramR GI GI GR :- !),
+  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "paramR:fail") C2),
+  coq.elpi.accumulate _ "derive.param2.db" (clause _ _ (param-done I)).
+
 }
 
 /*
diff --git a/apps/derive/tests/test_param2.v b/apps/derive/tests/test_param2.v
index 8e6924f61..bb61a1612 100644
--- a/apps/derive/tests/test_param2.v
+++ b/apps/derive/tests/test_param2.v
@@ -92,3 +92,12 @@ Definition size_seq (A : Type) : size_of (list A) := fun _ => 0.
 Elpi derive.param2 size_of.
 
 Elpi derive.param2 size_seq.  (* Fixed by https://github.com/LPCIC/coq-elpi/pull/754 *)
+
+Definition fa := 0.
+Definition fb := fa.
+
+Fail Elpi derive.param2 fb.
+
+Definition fa_R := O_R.
+Elpi derive.param2.register fa fa_R.
+Elpi derive.param2 fb.
diff --git a/apps/derive/theories/derive/param2.v b/apps/derive/theories/derive/param2.v
index 02af7d935..41120cfdc 100644
--- a/apps/derive/theories/derive/param2.v
+++ b/apps/derive/theories/derive/param2.v
@@ -54,6 +54,17 @@ Elpi Accumulate lp:{{
   usage :- coq.error "Usage: derive.param2 <object name>".
 }}. 
 
+Elpi Command derive.param2.register.
+Elpi Accumulate File param2.
+Elpi Accumulate Db derive.param2.db.
+Elpi Accumulate lp:{{
+  main [str I, str R] :- !, coq.locate I GRI, coq.locate R GRR,
+    derive.param2.main_register GRI GRR.
+  main _ :- usage.
+
+  usage :- coq.error "Usage: derive.param2.register <name> <name_R>".
+}}.
+
 
 (* hook into derive *)
 Elpi Accumulate derive File param2.

From 71daf5fc96f6c56a40bcc3e334f76874df47334b Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 28 Jan 2025 11:11:01 +0100
Subject: [PATCH 3/3] Document derive.param2 commands

---
 apps/derive/README.md | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/apps/derive/README.md b/apps/derive/README.md
index 9f36c00bd..ccb50992e 100644
--- a/apps/derive/README.md
+++ b/apps/derive/README.md
@@ -120,6 +120,34 @@ Inductive is_nat : nat -> Type :=
 | is_S : forall n : nat, is_nat n -> is_nat (S n) *)
 ```
 
+### `param2`
+
+Binary parametricity translation.
+
+Main command is `derive.param2`
+```coq
+Elpi derive.param2 nat.
+Print nat_R. (*
+Inductive nat_R : nat -> nat -> Set :=
+| O_R : nat_R 0 0
+| S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0).
+```
+
+The command `derive.param2.register` can be used to register
+handcrafted parametricity rules, so that they can be used by further
+`derive.param2` commands.
+```coq
+Definition fa := 0.
+Definition fb := fa.
+
+Fail Elpi derive.param2 fb.
+(* derive.param2: No binary parametricity translation for fa *)
+
+Definition fa_R := O_R.
+Elpi derive.param2.register fa fa_R.
+Elpi derive.param2 fb.
+```
+
 ### `param1_functor`
 
 ```coq