Avoid duplicates in the list.

[helm.git] / matita / components / ng_library / nCicLibrary.ml

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index edfb7db66782001b7efa68b2d2c253bff59e8a8f..cbc9c17b8b6809386ac2f5666d422135d1a3a829 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -260,7 +260,7 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
      D.set status
       (s#set_dump
         {s#dump with
-        includes = baseuri::s#dump.includes}) in
+        includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in
     let _dependencies,dump = require0 ~baseuri in
      List.fold_right (!require1 ~alias_only) dump status
    with