X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flexicon%2FlexiconSync.ml;h=30031943d9bb1897a5fa4a2a0dc473a715b7c796;hb=12ff38155f52e02b7e605a6970b997bc30eacb87;hp=d7fa27f902b2e7038ee46e7b3c9ed9986e025b47;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/lexicon/lexiconSync.ml b/components/lexicon/lexiconSync.ml index d7fa27f90..30031943d 100644 --- a/components/lexicon/lexiconSync.ml +++ b/components/lexicon/lexiconSync.ml @@ -41,7 +41,7 @@ let alias_diff ~from status = status.LexiconEngine.aliases [] let alias_diff = - let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in + let profiler = HExtlib.profile "alias_diff(conteg. anche in include)" in fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status (** given a uri and a type list (the contructors types) builds a list of pairs @@ -109,11 +109,3 @@ let time_travel ~present ~past = in List.iter CicNotation.remove_notation notation_to_remove -let init = - { - LexiconEngine.aliases = DisambiguateTypes.Environment.empty; - multi_aliases = DisambiguateTypes.Environment.empty; - lexicon_content_rev = []; - notation_ids = []; - metadata = []; - }