helm/software/components/ng_disambiguation/nDisambiguate.mli

   1
   2
   3 module Make (C : DisambiguateTypes.Callbacks) : sig
   4 val disambiguate_term :
   5     ?fresh_instances:bool ->
   6     dbd:HSql.dbd ->
   7     context:NCic.context ->
   8     metasenv:NCic.metasenv ->
   9     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
  10     universe:DisambiguateTypes.multiple_environment option ->
  11     CicNotationPt.term Disambiguate.disambiguator_input ->
  12     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
  13      NCic.metasenv *                  (* new metasenv *)
  14      NCic.term) list *  (* disambiguated term *)
  15     bool
  16 end