fix test

LPCIC · Oct 17, 2018 · 50eea33 · 50eea33
1 parent 1912082
commit 50eea33
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -20,3 +20,4 @@ About rtree_induction.
 Print rtree_eq.
 About rtree_eq_correct.
 Print rtree_eq_correct.
+Check rtree_eq_OK.