From f957bc90cc8d618af877bd16d75317e918d92e4a Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe@bedrocksystems.com>
Date: Thu, 15 Feb 2024 18:16:53 +0100
Subject: [PATCH] Simplify more.

---
 apps/derive/elpi/derive_synterp.elpi | 16 ++++++++--------
 apps/derive/theories/derive.v        |  6 +++---
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/apps/derive/elpi/derive_synterp.elpi b/apps/derive/elpi/derive_synterp.elpi
index 4185daa7e..1b56d0ac7 100644
--- a/apps/derive/elpi/derive_synterp.elpi
+++ b/apps/derive/elpi/derive_synterp.elpi
@@ -17,15 +17,15 @@ pred chain i:string, i:list derive.
 chain _ [].
 chain T [derive Name _ _|FS] :- not(selected Name), !,
   chain T FS.
-chain T [derive Name _ AlreadyDone|FS] :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
+chain T [derive _ _ AlreadyDone|FS] :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
   chain T FS.
-chain T [derive Name F _|FS] :- get-option "only" _, !, % request this one
+chain T [derive _ F _|FS] :- get-option "only" _, !, % request this one
   F _,
   chain T FS.
-chain T [derive Name F _|FS] :- % all are selected, we can fail
+chain T [derive _ F _|FS] :- % all are selected, we can fail
   (pi x\ stop x :- !, fail) => F _, !,
   chain T FS.
-chain T [derive F _ _|FS] :-
+chain T [derive _ _ _|FS] :-
   chain T FS.
 
 pred toposort i:list derive, o:list derive.
@@ -55,11 +55,11 @@ topo L Deps SL :-
   topo Other NewDeps SOther,
   std.append LNoDeps SOther SL.
 
-pred main i:string, i:bool, o:list prop.
-main T P CL :- main1 T P CL.
+pred main i:string, i:bool.
+main T P :- main1 T P.
 
-pred main1 i:string, i:bool, o:list prop.
-main1 T P CL :-
+pred main1 i:string, i:bool.
+main1 T P :-
   if (P = tt) (Prefix is T ^ "_") (Prefix = ""),
   std.findall (derivation T Prefix _) L,
   std.map L (x\r\ x = derivation _ _ r) DL,
diff --git a/apps/derive/theories/derive.v b/apps/derive/theories/derive.v
index 29ca05ecc..2bda372da 100644
--- a/apps/derive/theories/derive.v
+++ b/apps/derive/theories/derive.v
@@ -98,7 +98,7 @@ usage :-
 
 #[synterp] Elpi Accumulate lp:{{
   main [str I] :- !,
-    with-attributes (derive.main I tt _).
+    with-attributes (derive.main I tt).
 
   main [indt-decl D] :- !,
     with-attributes (with_name D).
@@ -110,11 +110,11 @@ usage :-
     pi p\ with_name (F p).
   with_name (inductive N _ _ _) :-
     coq.env.begin-module N none,
-    derive.main N tt _,
+    derive.main N tt,
     coq.env.end-module _.
   with_name (record N _ _ _) :-
     coq.env.begin-module N none,
-    derive.main N tt _,
+    derive.main N tt,
     coq.env.end-module _.
 }}.
 Elpi Typecheck.