Serious bug fixed: arities of coercions in the .moo files were not computed

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

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index d5eca252afe3f935ef740e1f0e2a76df02c9d1c1..4e64e6badc369c21d92e83d96c9719a4d72f1caa 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -293,9 +293,10 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
         let lemmas = 
           if add_composites then
             List.fold_left
-              (fun acc (_,_,uri,obj) -> 
+              (fun acc (_,tgt,uri,obj) -> 
                 add_single_obj uri obj refinement_toolkit;
-                uri::acc) 
+                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+                 (uri,arity)::acc) 
               [] new_coercions
           else
             []
@@ -358,6 +359,9 @@ let generate_projections refinement_toolkit uri fields =
          if coercion then
             begin
 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
+              (*CSC: I think there is a bug here. The composite coercions
+                are not remembered in the .moo file. Thus they are re-generated
+                every time. Right? *)
               let x = 
                 add_coercion ~add_composites:true refinement_toolkit uri arity
                 (UriManager.buri_of_uri uri)
@@ -366,7 +370,8 @@ let generate_projections refinement_toolkit uri fields =
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
   prerr_endline "---";
 *)
-              x
+              (*CSC: I throw the arity away. See comment above *)
+              List.map fst x
             end
           else  
             []