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_______________________________________________________________ *)
14 exception RefineFailure of (Stdpp.location * string) Lazy.t;;
15 exception Uncertain of (Stdpp.location * string) Lazy.t;;
16 exception AssertFailure of string Lazy.t;;
19 ?localize:(NCic.term -> Stdpp.location) ->
20 NCic.metasenv -> NCic.substitution -> NCic.context ->
21 NCic.term -> NCic.term option -> (* term, expected type *)
22 NCic.metasenv * NCic.substitution * NCic.term * NCic.term
23 (* menv, subst,refined term, type *)
26 exception RefineFailure of string Lazy.t;;
27 exception Uncertain of string Lazy.t;;
28 exception AssertFailure of string Lazy.t;;
30 (* type_of_aux' metasenv context term graph *)
31 (* refines [term] and returns the refined form of [term], *)
32 (* its type, the new metasenv and universe graph. *)
34 ?localization_tbl:Stdpp.location Cic.CicHash.t ->
35 Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
36 Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph
38 (* typecheck metasenv uri obj graph *)
39 (* refines [obj] and returns the refined form of [obj], *)
40 (* the new metasenv and universe graph. *)
41 (* the [uri] is required only for inductive definitions *)
43 localization_tbl:Stdpp.location Cic.CicHash.t ->
44 Cic.metasenv -> UriManager.uri option -> Cic.obj ->
45 Cic.obj * Cic.metasenv * CicUniv.universe_graph
47 val insert_coercions: bool ref (* initially true *)
49 val pack_coercion_obj: Cic.obj -> Cic.obj
51 val pack_coercion_metasenv: Cic.metasenv -> Cic.metasenv