Big commit to let Ferruccio try the merge_coercion patch.

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 457f376bb2c0afcb3b3540a68aeaca84f482d94e..430151d9a42fbd1594391aac8a1722bb4f8eff81 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -56,18 +56,3 @@ let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str =
       (Ulexing.from_utf8_string str) (fun _ _ -> ())
  with End_of_file -> ()
 
-let default_options () = no_options
-
-let initial_status =
-  lazy {
-    aliases = DisambiguateTypes.Environment.empty;
-    multi_aliases = DisambiguateTypes.Environment.empty;
-    moo_content_rev = [];
-    metadata = [];
-    proof_status = No_proof;
-    options = default_options ();
-    objects = [];
-    coercions = [];
-    notation_ids = [];
-  }
-