From 50eea33b4664dfa307ac0a0d17cac34a809961c4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gares@fettunta.org>
Date: Wed, 17 Oct 2018 11:40:00 +0200
Subject: [PATCH] fix test

---
 derive/derive.elpi              | 2 +-
 theories/tutorial/demo_derive.v | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

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.