X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Ftests%2Fdiscriminate.ma;h=d8e4bf2e25a84951c358c1437551c0d5a971d105;hb=2b2b90087f836c2f32291935216549e9370e68c3;hp=f873dd8f722e09d87d4ac5a3131bcbd0a356f196;hpb=b49f66c0d6f6e0606e98790f1d19683609e5196f;p=helm.git

diff --git a/helm/matita/tests/discriminate.ma b/helm/matita/tests/discriminate.ma
index f873dd8f7..d8e4bf2e2 100644
--- a/helm/matita/tests/discriminate.ma
+++ b/helm/matita/tests/discriminate.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/discriminate".
-include "coq.ma".
+include "legacy/coq.ma".
 alias id "not" = "cic:/Coq/Init/Logic/not.con".
 alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".