X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;fp=helm%2Fmatita%2FmatitaSync.ml;h=b06aedf30d7d5d4624af1a8a48c74169bd9bd94a;hb=18d9e31c73e22d03371d33b7b0a56418abf9b156;hp=66e3528bf9da3351cfe1f7cd81c80e5c8085d391;hpb=727ef55d2a6202a989c274f6caa1b0e1b7307880;p=helm.git

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 66e3528bf..b06aedf30 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -124,7 +124,18 @@ let add_obj uri obj status =
 let add_obj =
  let profiler = HExtlib.profile "add_obj" in
   fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
-   
+
+let add_coercion status ~add_composites uri =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let lemmas = CoercGraph.add_coercion ~basedir ~add_composites uri in
+ let status = {status with coercions = uri :: status.coercions} in
+ let statement_of name =
+   GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
+     (CicNotationPt.Ident (name, None)), false) in
+ let moo_content = [statement_of (UriManager.name_of_uri uri)] in
+ let status = MatitaTypes.add_moo_content moo_content status in
+  List.fold_left add_alias_for_constant status lemmas
+ 
 module OrderedUri =
 struct
   type t = UriManager.uri * string