added support for multi-aliases in disambiguation environment(s)

[helm.git] / helm / ocaml / cic_disambiguation / disambiguatePp.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index d6a33cfaedf76a1daa38daa1e1279a8d9f024d21..24f9ea37ea1b319f166cc17090fa4ec42564df7c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -49,7 +49,7 @@ let parse_environment str =
           Num instance,
           DisambiguateChoices.lookup_num_by_dsc desc
      in
-      environment := Environment.add key value !environment;
+      environment := Environment.cons key value !environment;
     done;
     assert false
   with End_of_file ->
@@ -58,18 +58,21 @@ let parse_environment str =
 let pp_environment env =
   let aliases =
     Environment.fold
-      (fun domain_item (dsc, _) acc ->
-        let s =
-          match domain_item with
-          | Id id ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "."
-          | Symbol (symb, i) ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc))
-              ^ "."
-          | Num i ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "."
-        in
-        s :: acc)
+      (fun domain_item codomain_items acc ->
+        List.fold_left
+          (fun strings (dsc, _) ->
+            let s =
+              match domain_item with
+              | Id id ->
+                  GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "."
+              | Symbol (symb, i) ->
+                  GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc))
+                  ^ "."
+              | Num i ->
+                  GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "."
+            in
+            s :: strings)
+          acc codomain_items)
       env []
   in
   String.concat "\n" (List.sort compare aliases)