Dead code removed (left from a previous commit).

[helm.git] / matita / components / lexicon / lexiconSync.ml

diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml
index 1971ac33e20f8ba04f601ab002f99c70fbe69834..e06c043722a2f03426666e9f86950f470c12066b 100644 (file)
--- a/matita/components/lexicon/lexiconSync.ml
+++ b/matita/components/lexicon/lexiconSync.ml
@@ -25,26 +25,6 @@
 
 (* $Id$ *)
 
-let alias_diff ~from status = 
-  let module Map = DisambiguateTypes.Environment in
-  Map.fold
-    (fun domain_item codomain_item acc ->
-      let description1 = LexiconAst.description_of_alias codomain_item in
-      try
-       let description2 = 
-          LexiconAst.description_of_alias 
-            (Map.find domain_item from#lstatus.LexiconEngine.aliases)
-       in
-        if description1 <> description2 then
-         (domain_item,codomain_item)::acc
-        else
-          acc
-      with
-       Not_found ->
-         (domain_item,codomain_item)::acc)
-    status#lstatus.LexiconEngine.aliases []
-;;
-
 let add_aliases_for_objs status =
  List.fold_left
   (fun status nref ->
@@ -54,34 +34,9 @@ let add_aliases_for_objs status =
       (fun u ->
         let name = NCicPp.r2s true u in
          DisambiguateTypes.Id name,
-          LexiconAst.Ident_alias (name,NReference.string_of_reference u)
+          GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
       ) references
     in
-     LexiconEngine.set_proof_aliases status new_env
+     GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
+      GrafiteAst.WithPreferences new_env
   ) status
- 
-module OrderedId = 
-struct
-  type t = CicNotation.notation_id
-  let compare =  CicNotation.compare_notation_id
-end
-
-module IdSet  = Set.Make (OrderedId)
-
-  (** @return l2 \ l1 *)
-let id_list_diff l2 l1 =
-  let module S = IdSet in
-  let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
-  let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
-  let diff = S.diff s2 s1 in
-  S.fold (fun uri uris -> uri :: uris) diff []
-
-let time_travel ~present ~past =
-  let notation_to_remove =
-    id_list_diff present#lstatus.LexiconEngine.notation_ids
-     past#lstatus.LexiconEngine.notation_ids
-  in
-   List.iter CicNotation.remove_notation notation_to_remove
-
-let push () = CicNotation.push ();;
-let pop () = CicNotation.pop ();;