GrafiteTypes.universe = universe},
lemmas
-let add_coercion refinement_toolkit ~add_composites status uri arity =
+let add_coercion refinement_toolkit ~add_composites status uri arity
+ saturations baseuri
+=
let compounds =
- LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity in
+ LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity
+ saturations baseuri in
{status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
compounds
List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
List.iter LibrarySync.remove_obj objs_to_remove
-let init () =
- LibrarySync.remove_all_coercions ();
- LibraryObjects.reset_defaults ();
- {
+let initial_status baseuri = {
GrafiteTypes.moo_content_rev = [];
proof_status = GrafiteTypes.No_proof;
- options = GrafiteTypes.no_options;
+(* options = GrafiteTypes.no_options; *)
objects = [];
coercions = [];
universe = Universe.empty;
+ baseuri = baseuri;
}
+
+
+let init baseuri =
+ LibrarySync.remove_all_coercions ();
+ LibraryObjects.reset_defaults ();
+ initial_status baseuri
+ ;;
+let pop () =
+ LibrarySync.pop ();
+ LibraryObjects.pop ()
+;;
+
+let push () =
+ LibrarySync.push ();
+ LibraryObjects.push ()
+;;
+