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 fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
24 mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
25 aliases:'alias DisambiguateTypes.Environment.t ->
26 universe:'alias list DisambiguateTypes.Environment.t option ->
27 rdb:#NRstatus.status ->
29 DisambiguateTypes.interactive_user_uri_choice_type ->
30 DisambiguateTypes.input_or_locate_uri_type ->
31 DisambiguateTypes.Environment.key ->
33 CicNotationPt.term Disambiguate.disambiguator_input ->
34 ((DisambiguateTypes.domain_item * 'alias) list *
40 val disambiguate_obj :
41 mk_implicit:(bool -> 'alias) ->
42 description_of_alias:('alias -> string) ->
43 fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
44 mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
45 aliases:'alias DisambiguateTypes.Environment.t ->
46 universe:'alias list DisambiguateTypes.Environment.t option ->
47 rdb:#NRstatus.status ->
49 DisambiguateTypes.interactive_user_uri_choice_type ->
50 DisambiguateTypes.input_or_locate_uri_type ->
51 DisambiguateTypes.Environment.key ->
54 string * int * CicNotationPt.term CicNotationPt.obj ->
55 ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv *
56 NCic.substitution * NCic.obj)
59 val disambiguate_path: CicNotationPt.term -> NCic.term