Several bugs fixed:

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

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index a4908ce7c893141cb040a42e640fb78c7a46e4c3..086893a974985e614026bfaebd29b89e5f4de912 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -405,12 +405,54 @@ let generate_inversion refinement_toolkit uri obj =
        add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
     (!build_inversion_principle uri obj)
 
+let
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
+=
+ function
+    Cic.Fix (_,funs) ->
+     snd (
+      List.fold_right
+       (fun (name,idx,ty,bo) (n,uris) ->
+         if name = name_to_avoid then
+          (n+1,uris)
+         else
+          let uri =
+           UriManager.uri_of_string
+            (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+          let bo = Cic.Fix (n,funs) in 
+          let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+           add_single_obj uri obj refinement_toolkit;
+           (n+1,uri::uris)
+       ) funs (1,[]))
+  | Cic.CoFix (_,funs) ->
+     snd (
+      List.fold_right
+       (fun (name,ty,bo) (n,uris) ->
+         if name = name_to_avoid then
+          (n+1,uris)
+         else
+          let uri =
+           UriManager.uri_of_string
+            (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+          let bo = Cic.CoFix (n,funs) in 
+          let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+           add_single_obj uri obj refinement_toolkit;
+           (n+1,uri::uris)
+       ) funs (1,[]))
+  | _ -> assert false
+
 let add_obj refinement_toolkit uri obj =
  add_single_obj uri obj refinement_toolkit;
  let uris = ref [] in
  try
   begin
    match obj with
+    | Cic.Constant (name,Some bo,_,_,attrs) when
+       List.mem (`Flavour `MutualDefinition) attrs ->
+        uris :=
+         !uris @
+           generate_sibling_mutual_definitions refinement_toolkit uri attrs
+            name bo
     | Cic.Constant _ -> ()
     | Cic.InductiveDefinition (_,_,_,attrs) ->
         uris := !uris @