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 disambiguate_term :
15 context:NCic.context ->
16 metasenv:NCic.metasenv ->
17 subst:NCic.substitution ->
18 expty:NCic.term option ->
19 mk_implicit: (bool -> 'alias) ->
20 description_of_alias:('alias -> string) ->
21 fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
22 mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
23 aliases:'alias DisambiguateTypes.Environment.t ->
24 universe:'alias list DisambiguateTypes.Environment.t option ->
25 rdb:#NCicCoercion.status ->
27 DisambiguateTypes.interactive_user_uri_choice_type ->
28 DisambiguateTypes.input_or_locate_uri_type ->
29 DisambiguateTypes.Environment.key ->
31 NotationPt.term Disambiguate.disambiguator_input ->
32 ((DisambiguateTypes.domain_item * 'alias) list *
38 val disambiguate_obj :
39 mk_implicit:(bool -> 'alias) ->
40 description_of_alias:('alias -> string) ->
41 fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
42 mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
43 aliases:'alias DisambiguateTypes.Environment.t ->
44 universe:'alias list DisambiguateTypes.Environment.t option ->
45 rdb:#NCicCoercion.status ->
47 DisambiguateTypes.interactive_user_uri_choice_type ->
48 DisambiguateTypes.input_or_locate_uri_type ->
49 DisambiguateTypes.Environment.key ->
52 string * int * NotationPt.term NotationPt.obj ->
53 ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv *
54 NCic.substitution * NCic.obj)
57 val disambiguate_path: NotationPt.term -> NCic.term