]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_disambiguation/nCicDisambiguate.mli
Fixed indentation, which is semantic in Haskell.
[helm.git] / matitaB / 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 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 -> GrafiteAst.alias_spec) ->
21   description_of_alias:(GrafiteAst.alias_spec -> string) ->
22   fix_instance:(DisambiguateTypes.domain_item -> GrafiteAst.alias_spec list -> GrafiteAst.alias_spec list) ->
23   mk_choice:(GrafiteAst.alias_spec -> NCic.term DisambiguateTypes.codomain_item) ->
24   aliases:GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t ->
25   universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
26   lookup_in_library:(
27     DisambiguateTypes.interactive_user_uri_choice_type ->
28     DisambiguateTypes.input_or_locate_uri_type ->
29     DisambiguateTypes.Environment.key ->
30     GrafiteAst.alias_spec list) ->
31   NotationPt.term Disambiguate.disambiguator_input ->
32   (GrafiteAst.alias_spec,NotationPt.term,NCic.metasenv,NCic.substitution,NCic.term,unit) Disambiguate.disamb_result
33   
34 val disambiguate_obj :
35   #NCicCoercion.status ->
36   mk_implicit:(bool -> GrafiteAst.alias_spec) ->
37   description_of_alias:(GrafiteAst.alias_spec -> string) ->
38   fix_instance:(DisambiguateTypes.domain_item -> GrafiteAst.alias_spec list -> GrafiteAst.alias_spec list) ->
39   mk_choice:(GrafiteAst.alias_spec -> NCic.term DisambiguateTypes.codomain_item) ->
40   aliases:GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t ->
41   universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
42   lookup_in_library:(
43     DisambiguateTypes.interactive_user_uri_choice_type ->
44     DisambiguateTypes.input_or_locate_uri_type ->
45     DisambiguateTypes.Environment.key ->
46      GrafiteAst.alias_spec list) ->
47   uri:NUri.uri ->
48   string * int * NotationPt.term NotationPt.obj ->
49   (GrafiteAst.alias_spec,NotationPt.term NotationPt.obj,NCic.metasenv,NCic.substitution,NCic.obj,unit) Disambiguate.disamb_result
50
51 val disambiguate_path: #NCicEnvironment.status -> NotationPt.term -> NCic.term