diff --git a/derive/derive.elpi b/derive/derive.elpi
index 53a40e58b..7c671fcd4 100644
--- a/derive/derive.elpi
+++ b/derive/derive.elpi
@@ -47,7 +47,7 @@ main T M :-
     derive.bcongr.main T {calc (Indname ^ "bcongr_")},
     derive.eqK.main T {calc (Indname ^ "eq_axiom_")},
     derive.eqcorrect.main T {calc (Indname ^ "eq_correct")},
-    derive.eqOK T {calc (Indname ^ "eq_OK")}
+    derive.eqOK.main T {calc (Indname ^ "eq_OK")}
   ].
   
 }
diff --git a/theories/tutorial/demo_derive.v b/theories/tutorial/demo_derive.v
index ed89a88e8..b37fbf833 100644
--- a/theories/tutorial/demo_derive.v
+++ b/theories/tutorial/demo_derive.v
@@ -20,3 +20,4 @@ About rtree_induction.
 Print rtree_eq.
 About rtree_eq_correct.
 Print rtree_eq_correct.
+Check rtree_eq_OK.