let lemmas =
LibrarySync.add_coercion ~add_composites ~pack_coercion_obj
uri arity saturations baseuri in
+ let status =
{ status with GrafiteTypes.coercions = CoercDb.dump () ;
- objects = lemmas @ status.GrafiteTypes.objects
- },
- lemmas
+ objects = lemmas @ status.GrafiteTypes.objects;
+ }
+ in
+ let db =
+ NCicCoercion.index_old_db (CoercDb.dump ())
+ (GrafiteTypes.get_coercions status)
+ in
+ let status = GrafiteTypes.set_coercions db status in
+ status, lemmas
let prefer_coercion s u =
CoercDb.prefer u;
coercions = CoercDb.empty_coerc_db;
automation_cache = AutomationCache.empty ();
baseuri = baseuri;
- ng_status = GrafiteTypes.CommandMode lexicon_status;
+ ng_status = GrafiteTypes.CommandMode {
+ NEstatus.lstatus = lexicon_status;
+ NEstatus.rstatus = {
+ NRstatus.uhint_db = NCicUnifHint.empty_db;
+ NRstatus.coerc_db = NCicCoercion.empty_db;
+ };
}
+}
let init baseuri =