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 #NCicCoercion.status ->
16 context:NCic.context ->
17 metasenv:NCic.metasenv ->
18 subst:NCic.substitution ->
19 expty:NCic.term option ->
20 mk_implicit: (bool -> 'alias) ->
21 description_of_alias:('alias -> string) ->
22 fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
23 mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
24 aliases:'alias DisambiguateTypes.Environment.t ->
25 universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
27 DisambiguateTypes.interactive_user_uri_choice_type ->
28 DisambiguateTypes.input_or_locate_uri_type ->
29 DisambiguateTypes.Environment.key ->
31 NotationPt.term Disambiguate.disambiguator_input ->
33 (DisambiguateTypes.domain_item * 'alias) list *
39 val disambiguate_obj :
40 #NCicCoercion.status ->
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:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
48 DisambiguateTypes.interactive_user_uri_choice_type ->
49 DisambiguateTypes.input_or_locate_uri_type ->
50 DisambiguateTypes.Environment.key ->
53 string * int * NotationPt.term NotationPt.obj ->
54 ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv *
55 NCic.substitution * NCic.obj)
58 val disambiguate_path: #NCic.status -> NotationPt.term -> NCic.term