diff --git a/apps/derive/README.md b/apps/derive/README.md
index f3f38ed22..d1210a4b9 100644
--- a/apps/derive/README.md
+++ b/apps/derive/README.md
@@ -7,33 +7,47 @@ given an inductive type declaration.
 
 ```coq
 From elpi.apps Require Import derive.std.
- 
-derive Inductive peano := Zero | Succ (p : peano).
 
-Print peano.
-(* Notation peano := peano.peano *)
+#[module] derive Inductive peano := Zero | Succ (p : peano).
+
 Print peano.peano.
-(* Inductive peano : Type :=  Zero : peano | Succ : peano -> peano *)
+(* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano. *)
 
 Eval compute in peano.eqb Zero (Succ Zero).
 (* = false : bool *)
 
 About peano.eqb_OK.
 (*
-peano.eqb_OK : forall x1 x2 : peano, Bool.reflect (x1 = x2) (peano.eqb x1 x2)
+peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (peano.eqb x1 x2)
 
 peano.eqb_OK is not universe polymorphic
 Arguments peano.eqb_OK x1 x2
 peano.eqb_OK is opaque
+Expands to: Constant elpi.apps.derive.examples.readme.peano.eqb_OK
 *)
 ```
 
-See also [examples/usage.v](examples/usage.v)
+See also [examples/usage.v](examples/usage.v) and [tests/test_readme.v](tests/test_readme.v).
 
 :warning: The line `From elpi.apps Require Import derive.std.` sets globally 
 `Uniform Inductive Parameters`.
 See the [documentation of that option in the Coq reference manual](https://coq.inria.fr/refman/language/core/inductive.html#coq:flag.Uniform-Inductive-Parameters).
 
+## Usage and attributes
+
+Using `derive Inductive ty := ...` produces the inductive `ty`, together with
+derivations, all in the current scope. The `#[module=<string>]` attriute can
+be used to specify that the inductive and the derivations should be wrapped
+in a module of the given name (the name of the inductive is used if no name
+is specified).
+
+When a wrapper module is generated, an alias (i.e., a notation) is generated
+for the inductive to be accessible with its name, outside of the module scope.
+This behaviour can be disabled by using the `#[no_alias]` boolean attribute.
+
+The `#[prefix=<string>]` attribute can be used to specify a prefix for all the
+derived definitions/lemmas.
+
 ## Documentation
 
 Elpi's `derive` app is a little framework to register derivations.
diff --git a/apps/derive/_CoqProject.test b/apps/derive/_CoqProject.test
index 346b3606b..34794415f 100644
--- a/apps/derive/_CoqProject.test
+++ b/apps/derive/_CoqProject.test
@@ -6,6 +6,7 @@
 -R tests    elpi.apps.derive.tests
 -R examples elpi.apps.derive.examples
 
+tests/test_readme.v
 tests/test_derive_stdlib.v
 tests/test_bcongr.v
 tests/test_derive.v
diff --git a/apps/derive/elpi/derive.elpi b/apps/derive/elpi/derive.elpi
index 5b55b1165..5733bd957 100644
--- a/apps/derive/elpi/derive.elpi
+++ b/apps/derive/elpi/derive.elpi
@@ -89,53 +89,84 @@ pred indt-or-const i:gref.
 indt-or-const (indt _).
 indt-or-const (const _).
 
-pred main i:gref, i:bool, o:list prop.
-main T P CL :- get-option "recursive" tt, !,
-  coq.env.dependencies T _ AllDeps,
+pred main i:gref, o:list prop.
+main GR CL :- get-option "module" M, !,
+  if (M = "") (coq.gref->id GR Mod) (Mod = M),
+  if-verbose (coq.say "Starting module" Mod),
+  coq.env.begin-module Mod none,
+  main-derive GR tt CL,
+  coq.env.end-module _.
+main GR CL :-
+  main-derive GR ff CL.
+
+pred main-derive i:gref, i:bool, o:list prop.
+main-derive GR InModule CL :- get-option "recursive" tt, !,
+  coq.env.dependencies GR _ AllDeps,
   coq.gref.set.elements AllDeps AllDepsL,
   std.filter AllDepsL indt-or-const Deps,
-  main.aux Deps [] CL1,
-  CL1 => main1 T P CL2,
+  main.aux InModule Deps [] CL1,
+  CL1 => main1 GR InModule CL2,
   std.append CL1 CL2 CL.
-pred main.aux i:list gref, i:list prop, o:list prop.
-main.aux [] X X.
-main.aux [T|TS] Acc CL :-
-  (pi X\get-option "only" X :- !, fail) => Acc => main T tt CL1,
-  main.aux TS {std.append CL1 Acc} CL.
-
-main T P CL :- main1 T P CL.
-
+main-derive GR InModule CL :- main1 GR InModule CL.
+
+pred main.aux i:bool, i:list gref, i:list prop, o:list prop.
+main.aux _ [] X X.
+main.aux InModule [GR|GRS] Acc CL :-
+  (pi X\get-option "only" X :- !, fail) => Acc => main-derive GR InModule CL1,
+  main.aux InModule GRS {std.append CL1 Acc} CL.
+
+pred validate-recursive i:prop, o:derive.
+validate-recursive (derivation _ _ tt _) _ :- get-option "recursive" tt,
+  coq.error "Synterp actions not supported in recursive derive.".
+validate-recursive (derivation _ _ _ R) R.
 pred main1 i:gref, i:bool, o:list prop.
-main1 T P CL :-
-  if (P = tt) (Prefix is {coq.gref->id T} ^ "_") (Prefix = ""),
-  std.findall (derivation T Prefix _) L,
+main1 GR InModule CL :-
+  if (get-option "prefix" PFX)
+     (Prefix = PFX)
+     (if (InModule is ff) (Prefix is {coq.gref->id GR} ^ "_") (Prefix = "")),
+  std.findall (derivation GR Prefix _ _) L,
   if (L = [])
      (coq.error "no derivation found, did you Import derive.std?")
      true,
-  std.map L (x\r\ x = derivation _ _ r) DL,
-  validate-only T DL,
+  std.map L validate-recursive DL,
+  validate-only GR DL,
   toposort DL SortedDL,
-  chain T SortedDL CL.
-
-pred decl+main i:indt-decl.
-decl+main DS :- std.do! [
-  indt-decl-name DS ModName,
-  if-verbose (coq.say "Starting module" ModName),
-  coq.env.begin-module ModName none,
+  chain GR SortedDL CL.
+
+pred decl+main i:string, i:indt-decl.
+decl+main TypeName DS :- std.do! [
+  if (get-option "module" M)
+     (if (M = "") (ModName = TypeName) (ModName = M), HasModule = tt)
+     (HasModule = ff),
+  if (HasModule = tt)
+     (if-verbose (coq.say "Starting module" ModName),
+      coq.env.begin-module ModName none)
+     true,
   std.assert-ok! (coq.elaborate-indt-decl-skeleton DS D) "Inductive type declaration illtyped",
   if-verbose (coq.say "Declaring inductive" D),
   coq.env.add-indt D I,
   if-verbose (coq.say "Deriving"),
-  main (indt I) ff CL,
+  main-derive (indt I) HasModule CL,
   if-verbose (coq.say "Done"),
-  coq.env.end-module _,
+  if (HasModule = tt)
+     (coq.env.end-module _,
+      decl+main.post TypeName I DS CL)
+     check-no-no-alias
+].
+
+pred check-no-no-alias.
+check-no-no-alias :- get-option "no_alias" tt, !,
+  coq.error "The no_alias attribute only has an effect when a wrapper module is generated.".
+check-no-no-alias.
 
+pred decl+main.post i:string, i:inductive, i:indt-decl, o:list prop.
+decl+main.post TypeName I DS CL :- std.do! [
   coq.env.indt I _ _ _ _ KS _,
   std.map KS (k\r\ r = indc k) KGRS,
   std.map KGRS coq.gref->id KNS,
   std.map KGRS (gr\r\ r = global gr) KTS,
 
-  std.forall2 [ModName|KNS] [global (indt I)|KTS] short-alias,
+  std.forall2 [TypeName|KNS] [global (indt I)|KTS] short-alias,
 
   coq.indt-decl->implicits DS IndImpls KsImpls,
   if (coq.any-implicit? IndImpls)
@@ -151,12 +182,7 @@ decl+main DS :- std.do! [
 ].
 
 pred short-alias i:id, i:term.
+short-alias _ _ :- get-option "no_alias" tt, !, true.
 short-alias ID T :- @global! => coq.notation.add-abbreviation ID 0 T ff _.
 
-pred indt-decl-name i:indt-decl, o:string.
-indt-decl-name (parameter _ _ _ Decl) Name :-
-  pi x\ indt-decl-name (Decl x) Name.
-indt-decl-name (inductive Name _ _ _) Name.
-indt-decl-name (record Name _ _ _) Name.
-
 }
diff --git a/apps/derive/elpi/derive_hook.elpi b/apps/derive/elpi/derive_hook.elpi
index 03c30d329..d80de7800 100644
--- a/apps/derive/elpi/derive_hook.elpi
+++ b/apps/derive/elpi/derive_hook.elpi
@@ -2,7 +2,7 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-pred derivation i:gref, i:string, o:derive.
+pred derivation i:gref, i:string, o:bool, o:derive.
 pred export i:modpath.
 pred dep1 o:string, o:string.
 kind derive type.
diff --git a/apps/derive/elpi/derive_synterp.elpi b/apps/derive/elpi/derive_synterp.elpi
new file mode 100644
index 000000000..1eae2a937
--- /dev/null
+++ b/apps/derive/elpi/derive_synterp.elpi
@@ -0,0 +1,80 @@
+/* Entry point for all derivations                                           */
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+
+namespace derive {
+
+pred dep o:string, o:string.
+dep X Y :- dep1 X Y.
+dep X Y :- dep1 X Z, dep Z Y.
+
+pred selected i:string.
+selected Name :- get-option "only" Map, !,
+  Map => (get-option Name _; (get-option X _, dep X Name)).
+selected _.
+
+pred chain i:string, i:list derive.
+chain _ [].
+chain T [derive Name _ _|FS] :- not(selected Name), !,
+  chain T FS.
+chain T [derive _ _ AlreadyDone|FS] :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
+  chain T FS.
+chain T [derive _ F _|FS] :- get-option "only" _, !, % request this one
+  F _,
+  chain T FS.
+chain T [derive _ F _|FS] :- % all are selected, we can fail
+  (pi x\ stop x :- !, fail) => F _, !,
+  chain T FS.
+chain T [derive _ _ _|FS] :-
+  chain T FS.
+
+pred toposort i:list derive, o:list derive.
+toposort L SL :-
+  std.findall (dep1 _ _) Deps,
+  topo L Deps SL.
+
+pred std.partition i:list A, i:(A -> prop), o:list A, o:list A.
+std.partition [] _ [] [].
+std.partition [X|XS] P [X|R] L :- P X, !, std.partition XS P R L.
+std.partition [X|XS] P R [X|L] :- std.partition XS P R L.
+
+pred not-a-src i:list prop, i:derive.
+not-a-src Deps (derive A _ _) :- not(std.mem! Deps (dep1 A _)).
+
+pred tgt-is-not-in i:list derive, i:prop.
+tgt-is-not-in [] _.
+tgt-is-not-in [derive Tgt _ _|_] (dep1 _ Tgt) :- !, fail.
+tgt-is-not-in [_|L] D :- tgt-is-not-in L D.
+
+pred topo i:list derive, i:list prop, o:list derive.
+topo [] _ [] :- !.
+topo L Deps SL :-
+  std.partition L (not-a-src Deps) LNoDeps Other,
+  if (LNoDeps = []) (coq.error "derive: no topological order:" L Deps) true,
+  std.filter Deps (tgt-is-not-in LNoDeps) NewDeps,
+  topo Other NewDeps SOther,
+  std.append LNoDeps SOther SL.
+
+pred main i:string.
+main TypeName :- get-option "module" M, !,
+  if (M = "") (Mod = TypeName) (Mod = M),
+  coq.env.begin-module Mod none,
+  main-derive TypeName tt,
+  coq.env.end-module _.
+main TypeName :-
+  main-derive TypeName ff.
+
+pred main-derive i:string, i:bool.
+main-derive TypeName InModule :- main1 TypeName InModule.
+
+pred main1 i:string, i:bool.
+main1 TypeName InModule :-
+  if (get-option "prefix" PFX)
+     (Prefix = PFX)
+     (if (InModule is ff) (Prefix is TypeName ^ "_") (Prefix = "")),
+  std.findall (derivation TypeName Prefix _) L,
+  std.map L (x\r\ x = derivation _ _ r) DL,
+  toposort DL SortedDL,
+  chain TypeName SortedDL.
+
+}
diff --git a/apps/derive/elpi/derive_synterp_hook.elpi b/apps/derive/elpi/derive_synterp_hook.elpi
new file mode 100644
index 000000000..80726a172
--- /dev/null
+++ b/apps/derive/elpi/derive_synterp_hook.elpi
@@ -0,0 +1,9 @@
+/* Entry point for derive extensions                                         */
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+
+pred derivation i:string, i:string, o:derive.
+pred export i:modpath.
+pred dep1 o:string, o:string.
+kind derive type.
+type derive string -> (list prop -> prop) -> prop -> derive.
diff --git a/apps/derive/examples/readme.v b/apps/derive/examples/readme.v
index 3be9f2d6d..5524a65a7 100644
--- a/apps/derive/examples/readme.v
+++ b/apps/derive/examples/readme.v
@@ -1,24 +1,22 @@
-(* README *)                            
+(* README *)
 From elpi.apps Require Import derive.std.
- 
-derive Inductive peano := Zero | Succ (p : peano).
 
-(* Bug 8.16: About peano.peano.*)
-(* Notation peano := peano.peano *)
+#[module] derive Inductive peano := Zero | Succ (p : peano).
 
 Print peano.peano.
-(* Inductive peano : Type :=  Zero : peano | Succ : peano -> peano *)
+(* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano. *)
 
 Eval compute in peano.eqb Zero (Succ Zero).
 (* = false : bool *)
 
 About peano.eqb_OK.
 (*
-peano.eqb_OK : forall x1 x2 : peano, Bool.reflect (x1 = x2) (peano.eqb x1 x2)
+peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (peano.eqb x1 x2)
 
 peano.eqb_OK is not universe polymorphic
 Arguments peano.eqb_OK x1 x2
 peano.eqb_OK is opaque
+Expands to: Constant elpi.apps.derive.examples.readme.peano.eqb_OK
 *)
 
 #[verbose] derive Nat.add.
@@ -26,4 +24,4 @@ Check is_add. (*
 : forall n : nat, is_nat n ->
   forall m : nat, is_nat m ->
     is_nat (n + m)
-*)
\ No newline at end of file
+*)
diff --git a/apps/derive/examples/usage.v b/apps/derive/examples/usage.v
index baa093925..42ec0bad8 100644
--- a/apps/derive/examples/usage.v
+++ b/apps/derive/examples/usage.v
@@ -7,7 +7,7 @@ From elpi.apps Require Import derive.std.
 Set Uniform Inductive Parameters.
 
 (** The best way to call derive is to prefix an Inductive declaration. *)
-derive
+#[module] derive
 Inductive tickle A := stop | more : A -> tickle -> tickle.
 
 (** The command is elaborated to something like:
@@ -40,7 +40,7 @@ Check tickle.tickle_R : (* relator (binary parametricity translation) *)
 (** This is a tricky case, since you need a good induction principle for the
     nested occurrence of tickle. #[verbose] prints all the derivations being
     run *)
-#[verbose] derive
+#[verbose,module] derive
 Inductive rtree A := Leaf (a : A) | Node (l : tickle rtree).
 
 Check rtree.induction : (* this is the key *)
@@ -50,7 +50,7 @@ Check rtree.induction : (* this is the key *)
   forall x, rtree.is_rtree A PA x -> P x.
 
 (** You can also select which derivations you like *)
-#[verbose, only(lens_laws, eqb)] derive
+#[verbose, only(lens_laws, eqb), module] derive
 Record Box A := { contents : A; tag : nat }.
 
 Check Box.eqb :
diff --git a/apps/derive/tests/test_derive.v b/apps/derive/tests/test_derive.v
index 670d4e489..773363c78 100644
--- a/apps/derive/tests/test_derive.v
+++ b/apps/derive/tests/test_derive.v
@@ -133,7 +133,7 @@ Check XXX.rtree_constructP : forall (A:Type) (l:rtree A), XXX.rtree_construct A
 Check XXX.rtree_eqb : forall (A:Type), (A -> A -> bool) -> rtree A -> rtree A -> bool.
 (* bug #270 *)
 
-derive
+#[module] derive
 Inductive triv : Coverage.unit -> Prop :=
 | one t : triv t | more x : triv x.
 
@@ -150,7 +150,7 @@ Inductive RoseTree : Type :=
 
 Elpi derive.param1 is_list.
 
-derive
+#[module] derive
 Inductive Pred : RoseTree -> Type :=
 | Pred_ctr branches :
     is_list _ Pred branches ->
diff --git a/apps/derive/tests/test_readme.v b/apps/derive/tests/test_readme.v
new file mode 100644
index 000000000..29a3c4a1b
--- /dev/null
+++ b/apps/derive/tests/test_readme.v
@@ -0,0 +1,100 @@
+From elpi.apps Require Import derive.std.
+
+Module example1.
+  derive Inductive peano := Zero | Succ (p : peano).
+
+  Print peano.
+  (* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano *)
+
+  Eval compute in peano_eqb Zero (Succ Zero).
+  (* = false : bool *)
+
+  Check peano_eqb_OK.
+  (* peano_eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (eqb x1 x2) *)
+End example1.
+
+Module example2.
+  #[module]
+  derive Inductive peano := Zero | Succ (p : peano).
+
+  Print peano.
+  (* Notation peano := peano.peano *)
+
+  Print peano.peano.
+  (* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano *)
+
+  Eval compute in peano.eqb Zero (Succ Zero).
+  (* = false : bool *)
+
+  Check peano.eqb_OK.
+  (* peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (eqb x1 x2) *)
+End example2.
+
+Module example3.
+  #[module="Peano"]
+  derive Inductive peano := Zero | Succ (p : peano).
+
+  Print peano.
+  (* Notation peano := Peano.peano *)
+
+  Print Peano.peano.
+  (* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano *)
+
+  Eval compute in Peano.eqb Zero (Succ Zero).
+  (* = false : bool *)
+
+  Check Peano.eqb_OK.
+  (* Peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (eqb x1 x2) *)
+End example3.
+
+Module example4.
+  #[module="Peano",prefix="Peano_"]
+  derive Inductive peano := Zero | Succ (p : peano).
+
+  Print peano.
+  (* Notation Peano := Peano.peano *)
+
+  Print Peano.peano.
+  (* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano *)
+
+  Print Module Peano.
+
+  Eval compute in Peano.Peano_eqb Zero (Succ Zero).
+  (* = false : bool *)
+
+  Check Peano.Peano_eqb_OK.
+  (* Peano.Peano_eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (eqb x1 x2) *)
+End example4.
+
+Module example5.
+  #[prefix=""]
+  derive Inductive peano := Zero | Succ (p : peano).
+
+  Print peano.
+  (* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano *)
+
+  Eval compute in eqb Zero (Succ Zero).
+  (* = false : bool *)
+
+  Check eqb_OK.
+  (* eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (eqb x1 x2) *)
+End example5.
+
+Module example6.
+  #[module=Peano,no_alias]
+    derive Inductive peano := Zero | Succ (p : peano).
+
+  Fail Print peano.
+
+  Print Peano.peano.
+  (* Inductive peano : Set := Peano.Zero : peano | Peano.Succ : peano -> peano *)
+
+  Eval compute in Peano.eqb Peano.Zero (Peano.Succ Peano.Zero).
+  (* = false : bool *)
+
+  Check Peano.eqb_OK.
+  (* Peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (eqb x1 x2) *)
+End example6.
+
+Fail #[no_alias]
+derive Inductive peano := Zero | Succ (p : peano).
diff --git a/apps/derive/theories/derive.v b/apps/derive/theories/derive.v
index 5d92cf97e..248e22df0 100644
--- a/apps/derive/theories/derive.v
+++ b/apps/derive/theories/derive.v
@@ -53,53 +53,65 @@
 *)
 
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 From elpi.apps.derive Extra Dependency "derive.elpi" as derive.
+From elpi.apps.derive Extra Dependency "derive_synterp.elpi" as derive_synterp.
 
 From elpi Require Import elpi.
 
 Elpi Command derive.
-Elpi Accumulate File derive_hook.
-Elpi Accumulate File derive.
 
+#[phase="both"]
 Elpi Accumulate lp:{{
+  % runs P in a context where Coq #[attributes] are parsed
+  pred with-attributes i:prop.
+  with-attributes P :-
+    attributes A,
+    coq.parse-attributes A [
+      att "verbose" bool,
+      att "only" attmap,
+      att "recursive" bool,
+      att "prefix" string,
+      att "module" string,
+      att "no_alias" bool,
+    ] Opts, !,
+    Opts => P.
+
+  pred get_name i:indt-decl, o:string.
+  get_name (parameter _ _ _ F) N :- pi p\ get_name (F p) N.
+  get_name (inductive N _ _ _) N.
+  get_name (record N _ _ _) N.
+}}.
 
-% runs P in a context where Coq #[attributes] are parsed
-pred with-attributes i:prop.
-with-attributes P :-
-  attributes A,
-  coq.parse-attributes A [
-    att "verbose" bool,
-    att "only" attmap,
-    att "recursive" bool,
-  ] Opts, !,
-  Opts => P.
-
-main [str I] :- !,
-  coq.locate I GR,
-  with-attributes (derive.main GR tt _).
+#[synterp] Elpi Accumulate File derive_synterp_hook.
+#[synterp] Elpi Accumulate File derive_synterp.
+#[synterp] Elpi Accumulate lp:{{
+  main [str TypeName] :- !,
+    with-attributes (derive.main TypeName).
 
-main [indt-decl D] :- !,
-  with-attributes (derive.decl+main D).
+  main [indt-decl D] :- !,
+    get_name D TypeName,
+    with-attributes (derive.main TypeName).
 
-main _ :- usage.
+  main _.
+}}.
 
-usage :-
-  coq.error "Usage:  derive <inductive type/definition>\n\tderive Inductive name Params : Arity := Constructors.".
+Elpi Accumulate File derive_hook.
+Elpi Accumulate File derive.
+Elpi Accumulate lp:{{
+  main [str I] :- !,
+    coq.locate I GR,
+    with-attributes (derive.main GR _).
 
-}}.
-#[synterp] Elpi Accumulate lp:{{
   main [indt-decl D] :- !,
-    declare-module-for-ind D.
-  main _.
+    get_name D TypeName,
+    with-attributes (derive.decl+main TypeName D).
 
-  pred declare-module-for-ind i:indt-decl.
-  declare-module-for-ind (parameter _ _ _ F) :-
-    pi p\ declare-module-for-ind (F p).
-  declare-module-for-ind (inductive N _ _ _) :-
-    coq.env.begin-module N none, coq.env.end-module _.
-  declare-module-for-ind (record N _ _ _) :-
-    coq.env.begin-module N none, coq.env.end-module _.
+  main _ :- usage.
 
+  usage :-
+    coq.error "Usage:  derive <inductive type/definition>\n\tderive Inductive name Params : Arity := Constructors.".
 }}.
+
 Elpi Typecheck.
 Elpi Export derive.
diff --git a/apps/derive/theories/derive/bcongr.v b/apps/derive/theories/derive/bcongr.v
index d9f14834b..9ea7a484e 100644
--- a/apps/derive/theories/derive/bcongr.v
+++ b/apps/derive/theories/derive/bcongr.v
@@ -6,6 +6,7 @@
 From elpi.apps.derive Extra Dependency "injection.elpi" as injection.
 From elpi.apps.derive Extra Dependency "bcongr.elpi" as bcongr.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From Coq Require Export Bool.
 From elpi Require Export elpi.
@@ -56,9 +57,17 @@ Elpi Typecheck.
 Elpi Accumulate derive Db derive.bcongr.db.
 Elpi Accumulate derive File injection.
 Elpi Accumulate derive File bcongr.
+
+#[phases=both] Elpi Accumulate derive lp:{{
+dep1 "bcongr" "projK".
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "bcongr" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
-dep1 "bcongr" "projK".
-derivation (indt T) N (derive "bcongr" (derive.bcongr.main T N) (derive.exists-indc T (K\bcongr-db K _))).
+derivation (indt T) N ff (derive "bcongr" (derive.bcongr.main T N) (derive.exists-indc T (K\bcongr-db K _))).
 
 }}.
diff --git a/apps/derive/theories/derive/eq.v b/apps/derive/theories/derive/eq.v
index ac5a1ec93..f813a7859 100644
--- a/apps/derive/theories/derive/eq.v
+++ b/apps/derive/theories/derive/eq.v
@@ -4,6 +4,7 @@
    ------------------------------------------------------------------------- *)
 From elpi.apps.derive Extra Dependency "eq.elpi" as eq.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From Coq Require Import Bool.
 From elpi Require Import elpi.
@@ -54,8 +55,13 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive Db derive.eq.db.
 Elpi Accumulate derive File eq.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "eq" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
-derivation (indt T) Prefix (derive "eq" (derive.eq.main T N) (eq-for T _)) :- N is Prefix ^ "eq".
+derivation (indt T) Prefix ff (derive "eq" (derive.eq.main T N) (eq-for T _)) :- N is Prefix ^ "eq".
 
 }}.
diff --git a/apps/derive/theories/derive/eqK.v b/apps/derive/theories/derive/eqK.v
index 831888138..07ba4a7f4 100644
--- a/apps/derive/theories/derive/eqK.v
+++ b/apps/derive/theories/derive/eqK.v
@@ -6,6 +6,7 @@
 From elpi.apps.derive Extra Dependency "discriminate.elpi" as discriminate.
 From elpi.apps.derive Extra Dependency "eqK.elpi" as eqK.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -65,10 +66,18 @@ Elpi Typecheck.
 Elpi Accumulate derive Db derive.eqK.db.
 Elpi Accumulate derive File discriminate.
 Elpi Accumulate derive File eqK.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "eqK" "bcongr".
 dep1 "eqK" "isK".
-derivation (indt T) Prefix (derive "eqK" (derive.eqK.main T N) (derive.exists-indc T (K\ eqK-db K _))) :- N is Prefix ^ "eq_axiom_".
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "eqK" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) Prefix ff (derive "eqK" (derive.eqK.main T N) (derive.exists-indc T (K\ eqK-db K _))) :- N is Prefix ^ "eq_axiom_".
 
 }}.
diff --git a/apps/derive/theories/derive/eqOK.v b/apps/derive/theories/derive/eqOK.v
index 1106584f5..b89d8f5fe 100644
--- a/apps/derive/theories/derive/eqOK.v
+++ b/apps/derive/theories/derive/eqOK.v
@@ -7,6 +7,7 @@ From elpi.apps.derive Extra Dependency "paramX_lib.elpi" as paramX.
 From elpi.apps.derive Extra Dependency "param1.elpi" as param1.
 From elpi.apps.derive Extra Dependency "eqOK.elpi" as eqOK.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -44,10 +45,18 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File eqOK.
 Elpi Accumulate derive Db derive.eqOK.db.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "eqOK" "eqcorrect".
 dep1 "eqOK" "param1_trivial".
-derivation (indt T) Prefix (derive "eqOK" (derive.eqOK.main T N) (eqOK-done T)) :- N is Prefix ^ "eq_OK".
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "eqOK" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) Prefix ff (derive "eqOK" (derive.eqOK.main T N) (eqOK-done T)) :- N is Prefix ^ "eq_OK".
 
 }}.
diff --git a/apps/derive/theories/derive/eqType_ast.v b/apps/derive/theories/derive/eqType_ast.v
index 81e4f1aae..e1be4bc3e 100644
--- a/apps/derive/theories/derive/eqType_ast.v
+++ b/apps/derive/theories/derive/eqType_ast.v
@@ -4,6 +4,7 @@ From elpi.apps Require Import derive.
 
 From elpi.apps.derive Extra Dependency "eqType.elpi" as eqType.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 Elpi Db derive.eqType.db lp:{{
 
@@ -52,8 +53,13 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive Db derive.eqType.db.
 Elpi Accumulate derive File eqType.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "eqType_ast" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
-derivation (indt T) _ (derive "eqType_ast" (derive.eqType.ast.main T) (eqType T _)).
+derivation (indt T) _ ff (derive "eqType_ast" (derive.eqType.ast.main T) (eqType T _)).
 
 }}.
diff --git a/apps/derive/theories/derive/eqb.v b/apps/derive/theories/derive/eqb.v
index f10484a3a..4c6a3868c 100644
--- a/apps/derive/theories/derive/eqb.v
+++ b/apps/derive/theories/derive/eqb.v
@@ -7,6 +7,7 @@ From elpi.apps.derive Extra Dependency "fields.elpi" as fields.
 From elpi.apps.derive Extra Dependency "eqb.elpi" as eqb.
 From elpi.apps.derive Extra Dependency "eqType.elpi" as eqType.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 Require Import eqb_core_defs.
 Require Import eqType_ast tag fields.
@@ -65,10 +66,18 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive Db derive.eqb.db.
 Elpi Accumulate derive File eqb.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "eqb" "fields".
-derivation (indt T)  Prefix (derive "eqb" (derive.eqb.main (indt T) Prefix) (eqb-done (indt T))).
-derivation (const C) Prefix (derive "eqb-alias" (derive.eqb.main (const C) Prefix) (eqb-done (const C))).
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "eqb" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T)  Prefix ff (derive "eqb" (derive.eqb.main (indt T) Prefix) (eqb-done (indt T))).
+derivation (const C) Prefix ff (derive "eqb-alias" (derive.eqb.main (const C) Prefix) (eqb-done (const C))).
 
 }}.
diff --git a/apps/derive/theories/derive/eqbOK.v b/apps/derive/theories/derive/eqbOK.v
index 0af93963b..ef31c547d 100644
--- a/apps/derive/theories/derive/eqbOK.v
+++ b/apps/derive/theories/derive/eqbOK.v
@@ -9,6 +9,7 @@ Require Import tag eqType_ast fields eqb eqbcorrect derive.
 From elpi.apps.derive Extra Dependency "eqbOK.elpi" as eqbOK.
 From elpi.apps.derive Extra Dependency "eqType.elpi" as eqType.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 Elpi Db derive.eqbOK.db lp:{{
 
@@ -42,11 +43,19 @@ Elpi Typecheck.
 (* hook into derive  *)
 Elpi Accumulate derive File eqbOK.
 Elpi Accumulate derive Db derive.eqbOK.db.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "eqbOK" "eqbcorrect".
-derivation (indt T) Prefix (derive "eqbOK" (derive.eqbOK.main (indt T) Prefix) (eqbok-for (indt T) _)).
 dep1 "eqbOK-alias" "eqbcorrect-alias".
-derivation (const T) Prefix (derive "eqbOK-alias" (derive.eqbOK.main (const T) Prefix) (eqbok-for (const T) _)).
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "eqbOK" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) Prefix ff (derive "eqbOK" (derive.eqbOK.main (indt T) Prefix) (eqbok-for (indt T) _)).
+derivation (const T) Prefix ff (derive "eqbOK-alias" (derive.eqbOK.main (const T) Prefix) (eqbok-for (const T) _)).
 
 }}.
diff --git a/apps/derive/theories/derive/eqbcorrect.v b/apps/derive/theories/derive/eqbcorrect.v
index 2f2033294..95f1dffaf 100644
--- a/apps/derive/theories/derive/eqbcorrect.v
+++ b/apps/derive/theories/derive/eqbcorrect.v
@@ -8,6 +8,7 @@ From elpi.apps.derive Extra Dependency "param1.elpi" as param1.
 From elpi.apps.derive Extra Dependency "eqType.elpi" as eqType.
 From elpi.apps.derive Extra Dependency "eqbcorrect.elpi" as eqbcorrect.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 Module Export exports.
 Export ssreflect ssrbool eqb_core_defs. (* go ask the ltac gurus... *)
@@ -96,13 +97,21 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File eqbcorrect.
 Elpi Accumulate derive Db derive.eqbcorrect.db.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "eqbcorrect" "eqb".
 dep1 "eqbcorrect" "induction".
 dep1 "eqbcorrect" "param1_inhab".
-derivation (indt T) Prefix (derive "eqbcorrect" (derive.eqbcorrect.main (indt T) Prefix) (eqcorrect-for (indt T) _ _)).
 dep1 "eqbcorrect-alias" "eqb-alias".
-derivation (const C) Prefix (derive "eqbcorrect-alias" (derive.eqbcorrect.main (const C) Prefix) (eqcorrect-for (const C) _ _)).
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "eqbcorrect" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) Prefix ff (derive "eqbcorrect" (derive.eqbcorrect.main (indt T) Prefix) (eqcorrect-for (indt T) _ _)).
+derivation (const C) Prefix ff (derive "eqbcorrect-alias" (derive.eqbcorrect.main (const C) Prefix) (eqcorrect-for (const C) _ _)).
 
 }}.
diff --git a/apps/derive/theories/derive/eqcorrect.v b/apps/derive/theories/derive/eqcorrect.v
index 0c4e143fe..312fb583c 100644
--- a/apps/derive/theories/derive/eqcorrect.v
+++ b/apps/derive/theories/derive/eqcorrect.v
@@ -5,6 +5,7 @@
 
 From elpi.apps.derive Extra Dependency "eqcorrect.elpi" as eqcorrect.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
   
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -54,12 +55,19 @@ Elpi Typecheck.
 Elpi Accumulate derive File derive_hook.
 Elpi Accumulate derive File eqcorrect.
 Elpi Accumulate derive Db derive.eqcorrect.db.
-Elpi Accumulate derive lp:{{
-  
+
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "eqcorrect" "induction".
 dep1 "eqcorrect" "eq".
 dep1 "eqcorrect" "eqK".
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "eqcorrect" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
 
-derivation (indt T) Prefix (derive "eqcorrect" (derive.eqcorrect.main T N) (eqcorrect-db (indt T) _)) :- N is Prefix ^ "eq_correct".
+derivation (indt T) Prefix ff (derive "eqcorrect" (derive.eqcorrect.main T N) (eqcorrect-db (indt T) _)) :- N is Prefix ^ "eq_correct".
 
 }}.
diff --git a/apps/derive/theories/derive/fields.v b/apps/derive/theories/derive/fields.v
index d91750ceb..1227f172d 100644
--- a/apps/derive/theories/derive/fields.v
+++ b/apps/derive/theories/derive/fields.v
@@ -5,6 +5,7 @@ From elpi.apps Require Export derive.eqType_ast derive.tag.
 From elpi.apps.derive Extra Dependency "fields.elpi" as fields.
 From elpi.apps.derive Extra Dependency "eqType.elpi" as eqType.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 Register unit as elpi.derive.unit.
 
@@ -51,10 +52,18 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File fields.
 Elpi Accumulate derive Db derive.fields.db.
-Elpi Accumulate derive lp:{{
-  
+
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "fields" "tag".
 dep1 "fields" "eqType_ast".
-derivation (indt T) Prefix (derive "fields" (derive.fields.main T Prefix) (fields-for T _ _ _ _)).
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "fields" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) Prefix ff (derive "fields" (derive.fields.main T Prefix) (fields-for T _ _ _ _)).
 
 }}.
diff --git a/apps/derive/theories/derive/idx2inv.v b/apps/derive/theories/derive/idx2inv.v
index caad9b655..448b91131 100644
--- a/apps/derive/theories/derive/idx2inv.v
+++ b/apps/derive/theories/derive/idx2inv.v
@@ -7,6 +7,7 @@ From elpi.apps.derive Extra Dependency "paramX_lib.elpi" as paramX.
 From elpi.apps.derive Extra Dependency "param1_functor.elpi" as param1_functor.
 From elpi.apps.derive Extra Dependency "idx2inv.elpi" as idx2inv.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Export elpi.
 From elpi.apps Require Export derive.
@@ -39,9 +40,17 @@ Elpi Typecheck.
 Elpi Accumulate derive Db derive.idx2inv.db.
 Elpi Accumulate derive File idx2inv.
 Elpi Accumulate File paramX.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "idx2inv" "invert".
-derivation (indt T) _ (derive "idx2inv" (derive.idx2inv.main T "_to_") (idx2inv-db T _ _ _)).
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "idx2inv" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) _ ff (derive "idx2inv" (derive.idx2inv.main T "_to_") (idx2inv-db T _ _ _)).
 
 }}.
diff --git a/apps/derive/theories/derive/induction.v b/apps/derive/theories/derive/induction.v
index 5fd5d4032..8946a339b 100644
--- a/apps/derive/theories/derive/induction.v
+++ b/apps/derive/theories/derive/induction.v
@@ -6,6 +6,7 @@ From elpi.apps.derive Extra Dependency "paramX_lib.elpi" as paramX.
 From elpi.apps.derive Extra Dependency "param1.elpi" as param1.
 From elpi.apps.derive Extra Dependency "induction.elpi" as induction.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive derive.param1 derive.param1_functor.
@@ -44,9 +45,17 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File induction.
 Elpi Accumulate derive Db derive.induction.db.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "induction" "param1_functor".
-derivation (indt T) N (derive "induction" (derive.induction.main T N) (induction-db T _)).
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "induction" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) N ff (derive "induction" (derive.induction.main T N) (induction-db T _)).
 
 }}.
diff --git a/apps/derive/theories/derive/invert.v b/apps/derive/theories/derive/invert.v
index 73e2c9444..f66638f18 100644
--- a/apps/derive/theories/derive/invert.v
+++ b/apps/derive/theories/derive/invert.v
@@ -5,6 +5,7 @@
    ------------------------------------------------------------------------- *)
 From elpi.apps.derive Extra Dependency "invert.elpi" as invert.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Export elpi.
 From elpi.apps Require Export derive.
@@ -26,8 +27,13 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File invert.
 Elpi Accumulate derive Db derive.invert.db.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "invert" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
-derivation (indt T) Prefix (derive "invert" (derive.invert.main T N) (invert-db (indt T) _)) :- N is Prefix ^ "inv".
+derivation (indt T) Prefix ff (derive "invert" (derive.invert.main T N) (invert-db (indt T) _)) :- N is Prefix ^ "inv".
 
 }}.
diff --git a/apps/derive/theories/derive/isK.v b/apps/derive/theories/derive/isK.v
index 48f649fdd..a1d66e91f 100644
--- a/apps/derive/theories/derive/isK.v
+++ b/apps/derive/theories/derive/isK.v
@@ -5,6 +5,7 @@
    ------------------------------------------------------------------------- *)
 From elpi.apps.derive Extra Dependency "isK.elpi" as isK.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -40,8 +41,13 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive Db derive.isK.db.
 Elpi Accumulate derive File isK.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "isK" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
-derivation (indt T) Prefix (derive "isK" (derive.isK.main T N) (derive.exists-indc T (K\ isK-db K _))) :- N is Prefix ^ "isk_".
+derivation (indt T) Prefix ff (derive "isK" (derive.isK.main T N) (derive.exists-indc T (K\ isK-db K _))) :- N is Prefix ^ "isk_".
 
 }}.
diff --git a/apps/derive/theories/derive/lens.v b/apps/derive/theories/derive/lens.v
index 36276a554..15a277146 100644
--- a/apps/derive/theories/derive/lens.v
+++ b/apps/derive/theories/derive/lens.v
@@ -4,6 +4,7 @@
    ------------------------------------------------------------------------- *)
 From elpi.apps.derive Extra Dependency "lens.elpi" as lens.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -46,6 +47,11 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive Db derive.lens.db.
 Elpi Accumulate derive File lens.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "lens" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
-  derivation (indt T) Prefix (derive "lens" (derive.lens.main T N) (lens-db T _ _)) :- N is Prefix ^ "_".
+  derivation (indt T) Prefix ff (derive "lens" (derive.lens.main T N) (lens-db T _ _)) :- N is Prefix ^ "_".
 }}.
diff --git a/apps/derive/theories/derive/lens_laws.v b/apps/derive/theories/derive/lens_laws.v
index 1af557549..89bf9b5ee 100644
--- a/apps/derive/theories/derive/lens_laws.v
+++ b/apps/derive/theories/derive/lens_laws.v
@@ -4,6 +4,7 @@
    ------------------------------------------------------------------------- *)
 From elpi.apps.derive Extra Dependency "lens_laws.elpi" as lens_laws.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.lens.
@@ -55,9 +56,17 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File lens_laws.
 Elpi Accumulate derive Db derive.lens_laws.db.
+
+#[phases=both] Elpi Accumulate derive lp:{{
+dep1 "lens_laws" "lens".
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "lens_laws" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
-dep1 "lens_laws" "lens".
-derivation (indt T) Prefix (derive "lens_laws" (derive.lens-laws.main T N) (lens-laws-done T)) :- N is Prefix ^ "_".
+derivation (indt T) Prefix ff (derive "lens_laws" (derive.lens-laws.main T N) (lens-laws-done T)) :- N is Prefix ^ "_".
 
 }}.
diff --git a/apps/derive/theories/derive/map.v b/apps/derive/theories/derive/map.v
index a18889512..c1edbffb5 100644
--- a/apps/derive/theories/derive/map.v
+++ b/apps/derive/theories/derive/map.v
@@ -4,6 +4,7 @@
    ------------------------------------------------------------------------- *)
 From elpi.apps.derive Extra Dependency "map.elpi" as map.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -34,6 +35,11 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive Db derive.map.db.
 Elpi Accumulate derive File map.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "map" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
-  derivation (indt T) N (derive "map" (derive.map.main T N) (map-done T)).
+  derivation (indt T) N ff (derive "map" (derive.map.main T N) (map-done T)).
 }}.
diff --git a/apps/derive/theories/derive/param1.v b/apps/derive/theories/derive/param1.v
index 3f7ef5758..3e5bb8303 100644
--- a/apps/derive/theories/derive/param1.v
+++ b/apps/derive/theories/derive/param1.v
@@ -5,6 +5,7 @@
 From elpi.apps.derive Extra Dependency "paramX_lib.elpi" as paramX.
 From elpi.apps.derive Extra Dependency "param1.elpi" as param1.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -102,11 +103,16 @@ Register is_eq as elpi.derive.is_eq.
 Elpi Accumulate derive File paramX.
 Elpi Accumulate derive File param1.
 Elpi Accumulate derive Db derive.param1.db.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "param1" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
 pred derive.on_param1 i:inductive, i:(inductive -> string -> list prop -> prop), i:string, o:list prop.
 derive.on_param1 T F N C :- reali (global (indt T)) (global (indt P)), !, F P N C.
 
-derivation T N (derive "param1" (derive.param1.main T N ) (reali-done T)).
+derivation T N ff (derive "param1" (derive.param1.main T N ) (reali-done T)).
 
 }}.
diff --git a/apps/derive/theories/derive/param1_congr.v b/apps/derive/theories/derive/param1_congr.v
index 86e529231..6631f9951 100644
--- a/apps/derive/theories/derive/param1_congr.v
+++ b/apps/derive/theories/derive/param1_congr.v
@@ -9,6 +9,7 @@
 From elpi.apps.derive Extra Dependency "paramX_lib.elpi" as paramX.
 From elpi.apps.derive Extra Dependency "param1_congr.elpi" as param1_congr.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Export elpi.
 From elpi.apps Require Export  derive.param1.
@@ -34,9 +35,17 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File param1_congr.
 Elpi Accumulate derive Db derive.param1.congr.db.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "param1_congr" "param1".
-derivation (indt T) _ (derive "param1_congr" (derive.on_param1 T derive.param1.congr.main "congr_") (derive.on_param1 T (T\_\_\derive.exists-indc T (K\ param1-congr-db K _)) _ _)).
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "param1_congr" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) _ ff (derive "param1_congr" (derive.on_param1 T derive.param1.congr.main "congr_") (derive.on_param1 T (T\_\_\derive.exists-indc T (K\ param1-congr-db K _)) _ _)).
 
 }}.
diff --git a/apps/derive/theories/derive/param1_functor.v b/apps/derive/theories/derive/param1_functor.v
index d1f3c2ffa..d43c18c0e 100644
--- a/apps/derive/theories/derive/param1_functor.v
+++ b/apps/derive/theories/derive/param1_functor.v
@@ -8,6 +8,7 @@
    ------------------------------------------------------------------------- *)
 From elpi.apps.derive Extra Dependency "param1_functor.elpi" as param1_functor.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -33,9 +34,17 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File param1_functor.
 Elpi Accumulate derive Db derive.param1.functor.db.
-Elpi Accumulate derive lp:{{
 
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "param1_functor" "param1".
-derivation (indt T) _ (derive "param1_functor" (derive.on_param1 T derive.param1.functor.main "_functor") (derive.on_param1 T (T\_\_\param1-functor-for T _ _) _ _)).
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "param1_functor" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
+
+derivation (indt T) _ ff (derive "param1_functor" (derive.on_param1 T derive.param1.functor.main "_functor") (derive.on_param1 T (T\_\_\param1-functor-for T _ _) _ _)).
 
 }}.
diff --git a/apps/derive/theories/derive/param1_trivial.v b/apps/derive/theories/derive/param1_trivial.v
index b3b6b5d49..0e754fa20 100644
--- a/apps/derive/theories/derive/param1_trivial.v
+++ b/apps/derive/theories/derive/param1_trivial.v
@@ -11,6 +11,7 @@ From elpi.apps.derive Extra Dependency "param1.elpi" as param1.
 From elpi.apps.derive Extra Dependency "param1_inhab.elpi" as param1_inhab.
 From elpi.apps.derive Extra Dependency "param1_trivial.elpi" as param1_trivial.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.param1 derive.param1_congr.
@@ -182,13 +183,20 @@ Elpi Typecheck.
 Elpi Accumulate derive Db derive.param1.trivial.db.
 Elpi Accumulate derive File param1_inhab.
 Elpi Accumulate derive File param1_trivial.
-Elpi Accumulate derive lp:{{
-  
+
+#[phases=both] Elpi Accumulate derive lp:{{
 dep1 "param1_trivial" "param1_inhab".
 dep1 "param1_trivial" "param1_congr".
 dep1 "param1_inhab" "param1".
+}}.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "param1_inhab" (cl\ cl = []) true).
+}}.
+
+Elpi Accumulate derive lp:{{
 
-derivation (indt T) _ (derive "param1_inhab"   (derive.on_param1 T derive.param1.inhab.main   "_inhab") (derive.on_param1 T (T\_\_\param1-inhab-done T) _ _)).
-derivation (indt T) _ (derive "param1_trivial" (derive.on_param1 T derive.param1.trivial.main "_trivial") (derive.on_param1 T (T\_\_\param1-trivial-done T) _ _)).
+derivation (indt T) _ ff (derive "param1_inhab"   (derive.on_param1 T derive.param1.inhab.main   "_inhab") (derive.on_param1 T (T\_\_\param1-inhab-done T) _ _)).
+derivation (indt T) _ ff (derive "param1_trivial" (derive.on_param1 T derive.param1.trivial.main "_trivial") (derive.on_param1 T (T\_\_\param1-trivial-done T) _ _)).
 
 }}.
diff --git a/apps/derive/theories/derive/param2.v b/apps/derive/theories/derive/param2.v
index a1b6367db..4be93df83 100644
--- a/apps/derive/theories/derive/param2.v
+++ b/apps/derive/theories/derive/param2.v
@@ -5,6 +5,7 @@
 From elpi.apps.derive Extra Dependency "paramX_lib.elpi" as paramX.
 From elpi.apps.derive Extra Dependency "param2.elpi" as param2.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -56,9 +57,14 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File param2.
 Elpi Accumulate derive Db derive.param2.db.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "param2" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
 
-derivation T N (derive "param2" (derive.param2.main T N) (param-done T)).
+derivation T N ff (derive "param2" (derive.param2.main T N) (param-done T)).
 
 }}.
 
diff --git a/apps/derive/theories/derive/projK.v b/apps/derive/theories/derive/projK.v
index 6c48a8306..101739063 100644
--- a/apps/derive/theories/derive/projK.v
+++ b/apps/derive/theories/derive/projK.v
@@ -7,6 +7,7 @@
    ------------------------------------------------------------------------- *)
 From elpi.apps.derive Extra Dependency "projK.elpi" as projK.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
@@ -40,8 +41,13 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive File projK.
 Elpi Accumulate derive Db derive.projK.db.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "projK" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
-derivation (indt T) Prefix (derive "projK" (derive.projK.main T N) (derive.exists-indc T (K\ projK-db K _ _))) :- N is Prefix ^ "getk_".
+derivation (indt T) Prefix ff (derive "projK" (derive.projK.main T N) (derive.exists-indc T (K\ projK-db K _ _))) :- N is Prefix ^ "getk_".
 
 }}.
diff --git a/apps/derive/theories/derive/tag.v b/apps/derive/theories/derive/tag.v
index f8e5f965d..f7927f667 100644
--- a/apps/derive/theories/derive/tag.v
+++ b/apps/derive/theories/derive/tag.v
@@ -3,6 +3,7 @@ From elpi.apps Require Import derive.
 From Coq Require Import PArith.
 From elpi.apps.derive Extra Dependency "tag.elpi" as tag.
 From elpi.apps.derive Extra Dependency "derive_hook.elpi" as derive_hook.
+From elpi.apps.derive Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
 Register positive as elpi.derive.positive.
 
@@ -39,8 +40,13 @@ Elpi Typecheck.
 (* hook into derive *)
 Elpi Accumulate derive Db derive.tag.db.
 Elpi Accumulate derive File tag.
+
+#[synterp] Elpi Accumulate derive lp:{{
+  derivation _ _ (derive "tag" (cl\ cl = []) true).
+}}.
+
 Elpi Accumulate derive lp:{{
   
-derivation (indt T) Prefix (derive "tag" (derive.tag.main T Prefix) (tag-for T _)).
+derivation (indt T) Prefix ff (derive "tag" (derive.tag.main T Prefix) (tag-for T _)).
 
 }}.