]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/dama/constructive_connectives.ma
matitadep sould be ok, outputs warning regarding issues and
[helm.git] / matita / dama / constructive_connectives.ma
index 8518d7ede45f0a68a07586f79ef1bccf4b219625..78e2ec571639f54103b6df1632df9c9022c7d577 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/constructive_connectives/".
+include "logic/connectives.ma".
 
 inductive Or (A,B:Type) : Type ≝
    Left : A → Or A B