metavariable context has a separator now

[helm.git] / helm / software / matita / contribs / dama / dama / russell_support.ma

diff --git a/helm/software/matita/contribs/dama/dama/russell_support.ma b/helm/software/matita/contribs/dama/dama/russell_support.ma
index bcaabd677baaedf5f9a35b93026e572a7a656d11..deb5fc950c628fbd01b4982a0f37a3b5db71b4f2 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/russell_support.ma
+++ b/helm/software/matita/contribs/dama/dama/russell_support.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "nat/nat.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
 
 definition hide ≝ λT:Type.λx:T.x.