if the user attempts to insert a duplicate coercions the system forbids it

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 1ca46db0bfd9538b3abb2d90e82b41762214213a..da2d69ec11352c6571b29673ae55391e37a2c743 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -314,8 +314,8 @@ and
              | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _)
              | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) -> 
                 (HLog.warn 
-                ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since " ^
-                "it is a duplicate of " ^ UriManager.string_of_uri u);
+                ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
+                 "it is a duplicate of " ^ UriManager.string_of_uri u);
                 true) 
              | CoercDb.Sort s1, CoercDb.Sort s2 -> 
               (HLog.warn 
@@ -326,19 +326,21 @@ and
                  CicPp.ppterm (Cic.Sort s2)); false)
              | _ -> 
                 (HLog.warn 
-                ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since " ^
-                "it is a duplicate of " ^ UriManager.string_of_uri u);
+                ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
+                 "it is a duplicate of " ^ UriManager.string_of_uri u);
                 true))
          ul)
       (CoercDb.to_list ())
   in
   let cpos = no_args - arity - saturations - 1 in 
   if not add_composites then
-    (ignore(already_in_obj src_carr tgt_carr uri 
-      (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)));
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
-    []))
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); [])
   else
+    let _ = 
+      if already_in_obj src_carr tgt_carr uri
+       (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)) then
+        raise (AlreadyDefined uri);
+    in
     let new_coercions = 
       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
        baseuri
@@ -348,18 +350,17 @@ and
       new_coercions 
     in
     (* update the DB *)
-    ignore(already_in_obj src_carr tgt_carr uri 
-      (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)));
-    List.iter 
-      (fun (src,tgt,uri,saturations,_,_,cpos) ->
-        CoercDb.add_coercion (src,tgt,uri,saturations,cpos)) 
-      new_coercions;
+    let lemmas = 
+      List.fold_left
+        (fun acc (src,tgt,uri,saturations,obj,arity,cpos) ->
+           CoercDb.add_coercion (src,tgt,uri,saturations,cpos);
+           let acc = add_obj uri obj pack_coercion_obj @ uri::acc in
+           acc)
+        [] new_coercions
+    in
     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
-    (* add the composites obj and they eventual lemmas *)
-      (List.fold_left
-        (fun acc (_,tgt,uri,saturations,obj,arity,cpos) -> 
-          add_obj uri obj pack_coercion_obj @ uri::acc)
-        [] new_coercions)
+(*     CoercDb.prefer uri; *)
+    lemmas
 ;;