From cc3a8b5a720b89afac5a4d90456754aa9b53c637 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 5 Oct 2005 16:10:53 +0000 Subject: [PATCH] s/commands_of_domain_and_codomain_items_list/aliases_of_domain_and_codomain_items_list/ --- helm/ocaml/cic_disambiguation/disambiguatePp.ml | 5 ----- helm/ocaml/cic_disambiguation/disambiguatePp.mli | 6 +++--- 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml index 1f25e1f95..c3a48e409 100644 --- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml +++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml @@ -75,11 +75,6 @@ let aliases_of_domain_and_codomain_items_list l = alias_of_domain_and_codomain_items domain_item codomain_item::acc ) [] l -let commands_of_domain_and_codomain_items_list l = - List.map - (fun alias -> GrafiteAst.Alias (dummy_floc, alias)) - (aliases_of_domain_and_codomain_items_list l) - let pp_environment env = let aliases = aliases_of_environment env in let strings = diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.mli b/helm/ocaml/cic_disambiguation/disambiguatePp.mli index 9c3b50661..69b6e8451 100644 --- a/helm/ocaml/cic_disambiguation/disambiguatePp.mli +++ b/helm/ocaml/cic_disambiguation/disambiguatePp.mli @@ -27,8 +27,8 @@ val parse_environment: string -> DisambiguateTypes.environment * DisambiguateTypes.multiple_environment -val commands_of_domain_and_codomain_items_list: - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> - (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list +val aliases_of_domain_and_codomain_items_list: + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> + GrafiteAst.alias_spec list val pp_environment: DisambiguateTypes.environment -> string -- 2.39.2