]> matita.cs.unibo.it Git - helm.git/commitdiff
Avoid duplicates in the list.
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 23 Dec 2010 12:13:32 +0000 (12:13 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 23 Dec 2010 12:13:32 +0000 (12:13 +0000)
matita/components/ng_library/nCicLibrary.ml

index edfb7db66782001b7efa68b2d2c253bff59e8a8f..cbc9c17b8b6809386ac2f5666d422135d1a3a829 100644 (file)
@@ -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