(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id$ *)

(*
exception RefineFailure of string Lazy.t;;
exception Uncertain of string Lazy.t;;
exception AssertFailure of string Lazy.t;;

(* type_of_aux' metasenv context term graph                *)
(* refines [term] and returns the refined form of [term],  *)
(* its type, the new metasenv and universe graph.          *)
val type_of_aux':
 ?localization_tbl:Stdpp.location Cic.CicHash.t ->
  Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
   Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph

(* typecheck metasenv uri obj graph                     *)
(* refines [obj] and returns the refined form of [obj], *)
(* the new metasenv and universe graph.                 *)
(* the [uri] is required only for inductive definitions *)
val typecheck : 
 localization_tbl:Stdpp.location Cic.CicHash.t ->
  Cic.metasenv -> UriManager.uri option -> Cic.obj ->
   Cic.obj * Cic.metasenv * CicUniv.universe_graph

val insert_coercions: bool ref (* initially true *)

val pack_coercion_obj: Cic.obj -> Cic.obj

val pack_coercion_metasenv: Cic.metasenv -> Cic.metasenv
*)