X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Flibrary%2FlibrarySync.ml;h=922955aa0af384c3e16716c8942c2097d225426a;hb=caa84292498037f8cadcb1d200a69dec3b66c0ea;hp=fe631edd2e761579b8d70c27c24490f87c861d4a;hpb=aa0d60227b785da3355b31519ba11cb4fbd2c925;p=helm.git

diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml
index fe631edd2..922955aa0 100644
--- a/helm/ocaml/library/librarySync.ml
+++ b/helm/ocaml/library/librarySync.ml
@@ -50,7 +50,7 @@ let merge_coercions obj =
         C.Lambda (name, aux so, aux dest)
     | C.LetIn (name,so,dest) -> 
         C.LetIn (name, aux so, aux dest)
-    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when 
+    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when 
       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
         let source_carr = CoercGraph.source_of c2 in
         let tgt_carr = CoercGraph.target_of c1 in
@@ -180,7 +180,7 @@ let index_obj =
 
 let add_single_obj uri obj ~basedir =
   let obj = 
-    if List.mem `Generated (CicUtil.attributes_of_obj obj) &&
+    if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
        not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
     then
       merge_coercions obj