Yet another implementation of the single aliases / multi aliases idea.

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 8c891b04355759f28ff7a8522329fed6dcb54293..577e243a6744879152b0706965c3dde1ff8afddd 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -165,7 +165,8 @@ let disambiguate_term status_ref term =
   let (aliases, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
+        ~aliases:status.aliases ~universe:(Some status.multi_aliases)
+        ~context:(MatitaMisc.get_proof_context status)
         ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
   in
   let status = MatitaTypes.set_metasenv metasenv status in
@@ -184,8 +185,8 @@ let disambiguate_lazy_term status_ref term =
     let (aliases, metasenv, cic, ugraph) =
       singleton
         (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
-          ~initial_ugraph:ugraph ~aliases:status.aliases ~context ~metasenv
-            term)
+          ~initial_ugraph:ugraph ~aliases:status.aliases
+          ~universe:(Some status.multi_aliases) ~context ~metasenv term)
     in
     let status = MatitaTypes.set_metasenv metasenv status in
     let status = MatitaSync.set_proof_aliases status aliases in
@@ -511,7 +512,7 @@ let disambiguate_obj status obj =
   let (aliases, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~uri obj)
+        ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
   in
   let proof_status =
     match status.proof_status with
@@ -628,17 +629,17 @@ let eval_command opts status cmd =
              code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
-         DisambiguateTypes.Environment.cons
+         DisambiguateTypes.Environment.add
           (DisambiguateTypes.Id id) 
           (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
           status.aliases 
       | GrafiteAst.Symbol_alias (symb, instance, desc) ->
-         DisambiguateTypes.Environment.cons
+         DisambiguateTypes.Environment.add
           (DisambiguateTypes.Symbol (symb,instance))
           (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
           status.aliases
       | GrafiteAst.Number_alias (instance,desc) ->
-         DisambiguateTypes.Environment.cons
+         DisambiguateTypes.Environment.add
           (DisambiguateTypes.Num instance)
           (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
      in
@@ -648,7 +649,7 @@ let eval_command opts status cmd =
   | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
       let status' = add_moo_content [stm] status in
       let aliases' =
-        DisambiguateTypes.Environment.cons
+        DisambiguateTypes.Environment.add
           (DisambiguateTypes.Symbol (symbol, 0))
           (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
           status.aliases
@@ -800,7 +801,8 @@ let default_options () =
 
 let initial_status =
   lazy {
-    aliases = DisambiguateTypes.empty_environment;
+    aliases = DisambiguateTypes.Environment.empty;
+    multi_aliases = DisambiguateTypes.Environment.empty;
     moo_content_rev = [];
     proof_status = No_proof;
     options = default_options ();