X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.mli;h=0e05413b8d68c0aeaaad68e2c2b221e949f29f69;hb=b38de2d3fa8bbe346c59c18bbeb889f29e493f63;hp=94690373af3abe9f368b230225e43cab3e61de18;hpb=308d03101d84a4d62465bb3ff7c0cd9ca866c659;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 94690373a..0e05413b8 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -23,19 +23,7 @@ * http://helm.cs.unibo.it/ *) -open Disambiguate_types - -(** {2 Choice registration interface} *) - - (** to be raised when a choice is invalid due to some given parameter (e.g. - * wrong number of Cic.term arguments received) *) -exception Invalid_choice - - (** register a new symbol choice *) -val add_symbol_choice: string -> codomain_item -> unit - - (** register a new number choice *) -val add_num_choice: codomain_item -> unit +open DisambiguateTypes (** {2 Disambiguation interface} *) @@ -47,7 +35,7 @@ module Make (C : Callbacks) : MQIConn.handle -> Cic.context -> Cic.metasenv -> - Ast.term -> + CicAst.term -> aliases:environment -> (* previous interpretation status *) environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *)