]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_disambiguation/nCicDisambiguate.mli
made executable again
[helm.git] / matita / components / ng_disambiguation / nCicDisambiguate.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 val debug : bool ref
15
16 val disambiguate_term :
17   #NCicCoercion.status ->
18   context:NCic.context ->
19   metasenv:NCic.metasenv -> 
20   subst:NCic.substitution ->
21   expty:NCic.term NCicRefiner.expected_type ->
22   mk_implicit: (bool -> 'alias) ->
23   description_of_alias:('alias -> string) ->
24   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
25   mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
26   aliases:'alias DisambiguateTypes.Environment.t ->
27   universe:'alias list DisambiguateTypes.Environment.t option ->
28   lookup_in_library:(
29     DisambiguateTypes.interactive_user_uri_choice_type ->
30     DisambiguateTypes.input_or_locate_uri_type ->
31     DisambiguateTypes.Environment.key ->
32     'alias list) ->
33   NotationPt.term Disambiguate.disambiguator_input ->
34   ((DisambiguateTypes.domain_item * 'alias) list *
35    NCic.metasenv *                  
36    NCic.substitution *
37    NCic.term) list * 
38   bool
39   
40 val disambiguate_obj :
41   #NCicCoercion.status ->
42   mk_implicit:(bool -> 'alias) ->
43   description_of_alias:('alias -> string) ->
44   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
45   mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
46   aliases:'alias DisambiguateTypes.Environment.t ->
47   universe:'alias list DisambiguateTypes.Environment.t option ->
48   lookup_in_library:(
49     DisambiguateTypes.interactive_user_uri_choice_type ->
50     DisambiguateTypes.input_or_locate_uri_type ->
51     DisambiguateTypes.Environment.key ->
52      'alias list) ->
53   uri:NUri.uri ->
54   string * int * NotationPt.term NotationPt.obj ->
55   ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv *
56    NCic.substitution * NCic.obj)
57   list * bool
58
59 val disambiguate_path: #NCic.status -> NotationPt.term -> NCic.term