]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/Makefile
Automatic generation of elimination and inversion principles for co-inductive
[helm.git] / helm / software / components / library / Makefile
index 013f5f4a0246b2168697cce2fbb748dab354c865..e3c921dd7dc21c752616f1b779e042e1af962232 100644 (file)
@@ -2,6 +2,7 @@ PACKAGE = library
 PREDICATES =
 
 INTERFACE_FILES = \
+       librarian.mli \
        cicElim.mli \
        cicRecord.mli \
        libraryMisc.mli \
@@ -9,7 +10,6 @@ INTERFACE_FILES = \
        coercDb.mli \
        cicCoercion.mli \
        librarySync.mli \
-       libraryNoDb.mli \
        libraryClean.mli \
        $(NULL)
 IMPLEMENTATION_FILES = \