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     subst:NCic.substitution ->
  10     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
  11     universe:DisambiguateTypes.multiple_environment option ->
  12     ?goal: int ->
  13     CicNotationPt.term Disambiguate.disambiguator_input ->
  14     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
  15      NCic.metasenv *                  (* new metasenv *)
  16      NCic.substitution *
  17      NCic.term) list *  (* disambiguated term *)
  18     bool
  19 end