helm/software/components/ng_disambiguation/nDisambiguate.mli

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 module Make (C : DisambiguateTypes.Callbacks) : sig
  15 val disambiguate_term :
  16     ?fresh_instances:bool ->
  17     context:NCic.context ->
  18     metasenv:NCic.metasenv ->
  19     subst:NCic.substitution ->
  20     aliases:NCic.term DisambiguateTypes.environment ->(* previous interpretation status *)
  21     universe:NCic.term DisambiguateTypes.multiple_environment option ->
  22     lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
  23                         ?ok:string ->
  24                         ?enable_button_for_non_vars:bool ->
  25                         title:string ->
  26                         msg:string ->
  27                         id:string ->
  28                         UriManager.uri list -> UriManager.uri list) ->
  29                        (title:string -> ?id:string -> unit -> UriManager.uri option) ->
  30                        DisambiguateTypes.Environment.key ->
  31                        NCic.term DisambiguateTypes.codomain_item list) ->
  32     ?goal: int ->
  33     CicNotationPt.term Disambiguate.disambiguator_input ->
  34     ((DisambiguateTypes.domain_item * NCic.term DisambiguateTypes.codomain_item) list *
  35      NCic.metasenv *                  (* new metasenv *)
  36      NCic.substitution *
  37      NCic.term) list *  (* disambiguated term *)
  38     bool
  39 end