Composition of coercions with arity > 0 is now implemented correctly.

[helm.git] / components / library / librarySync.ml

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 5897d62ba8c81256b3213af333c9a1d0cbf03baa..5189547d33135903df0731105a50fa99041b2f91 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -314,13 +314,13 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        baseuri
     in
     let new_coercions = 
-      List.filter (fun (s,t,u,saturations,obj) -> not(already_in_obj s t u obj))
+      List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
       new_coercions 
     in
-    let composite_uris = List.map (fun (_,_,uri,_,_) -> uri) new_coercions in
+    let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
     (* update the DB *)
     List.iter 
-      (fun (src,tgt,uri,saturations,_) ->
+      (fun (src,tgt,uri,saturations,_,_) ->
         CoercDb.add_coercion (src,tgt,uri,saturations)) 
       new_coercions;
     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
@@ -328,9 +328,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     let lemmas = 
       if add_composites then
         List.fold_left
-          (fun acc (_,tgt,uri,saturations,obj) -> 
+          (fun acc (_,tgt,uri,saturations,obj,arity) -> 
             add_single_obj uri obj refinement_toolkit;
-            let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
              (uri,arity,saturations)::acc) 
           [] new_coercions
       else