moved coercions away (work in progress)

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 66e3528bf9da3351cfe1f7cd81c80e5c8085d391..b06aedf30d7d5d4624af1a8a48c74169bd9bd94a 100644 (file)
--- 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