3 Copyright (C) 1999-2006, HELM Team.
5 This file is part of HELM, an Hypertextual, Electronic
6 Library of Mathematics, developed at the Computer Science
7 Department, University of Bologna, Italy.
9 HELM is free software; you can redistribute it and/or
10 modify it under the terms of the GNU General Public License
11 as published by the Free Software Foundation; either version 2
12 of the License, or (at your option) any later version.
14 HELM is distributed in the hope that it will be useful,
15 but WITHOUT ANY WARRANTY; without even the implied warranty of
16 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17 GNU General Public License for more details.
19 You should have received a copy of the GNU General Public License
20 along with this program; if not, write to the Free Software
21 Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
24 For details, see the HELM web site: http://helm.cs.unibo.it/
27 val interpretate_path :
28 context:Cic.name list -> CicNotationPt.term -> Cic.term
30 val disambiguate_term :
31 context:Cic.context ->
32 metasenv:Cic.metasenv ->
33 subst:Cic.substitution ->
35 ?initial_ugraph:CicUniv.universe_graph ->
36 aliases:Cic.term DisambiguateTypes.environment ->
37 universe:Cic.term DisambiguateTypes.multiple_environment option ->
39 DisambiguateTypes.interactive_user_uri_choice_type ->
40 DisambiguateTypes.input_or_locate_uri_type ->
41 DisambiguateTypes.Environment.key ->
42 Cic.term DisambiguateTypes.codomain_item list) ->
43 CicNotationPt.term Disambiguate.disambiguator_input ->
44 ((DisambiguateTypes.domain_item *
45 Cic.term DisambiguateTypes.codomain_item) list *
49 CicUniv.universe_graph) list *
52 val disambiguate_obj :
53 aliases:Cic.term DisambiguateTypes.environment ->
54 universe:Cic.term DisambiguateTypes.multiple_environment option ->
55 uri:UriManager.uri option -> (* required only for inductive types *)
57 DisambiguateTypes.interactive_user_uri_choice_type ->
58 DisambiguateTypes.input_or_locate_uri_type ->
59 DisambiguateTypes.Environment.key ->
60 Cic.term DisambiguateTypes.codomain_item list) ->
61 CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input ->
62 ((DisambiguateTypes.domain_item *
63 Cic.term DisambiguateTypes.codomain_item) list *
67 CicUniv.universe_graph) list *