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.
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_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
14 val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
16 val disambiguate_term :
17 context:NCic.context ->
18 metasenv:NCic.metasenv ->
19 subst:NCic.substitution ->
20 expty:NCic.term option ->
21 mk_implicit: (bool -> 'alias) ->
22 description_of_alias:('alias -> string) ->
23 mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
24 aliases:'alias DisambiguateTypes.Environment.t ->
25 universe:'alias list DisambiguateTypes.Environment.t option ->
26 rdb:#NRstatus.status ->
28 DisambiguateTypes.interactive_user_uri_choice_type ->
29 DisambiguateTypes.input_or_locate_uri_type ->
30 DisambiguateTypes.Environment.key ->
32 CicNotationPt.term Disambiguate.disambiguator_input ->
33 ((DisambiguateTypes.domain_item * 'alias) list *
39 val disambiguate_obj :
40 mk_implicit:(bool -> 'a) ->
41 description_of_alias:('a -> string) ->
42 mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) ->
43 aliases:'a DisambiguateTypes.Environment.t ->
44 universe:'a list DisambiguateTypes.Environment.t option ->
45 rdb:#NRstatus.status ->
46 lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type ->
47 DisambiguateTypes.input_or_locate_uri_type ->
48 DisambiguateTypes.Environment.key -> 'a list) ->
50 string * int * CicNotationPt.term CicNotationPt.obj ->
51 ((DisambiguateTypes.Environment.key * 'a) list * NCic.metasenv *
52 NCic.substitution * NCic.obj)
55 val disambiguate_path: CicNotationPt.term -> NCic.term