exception Impossible of int
exception NotWellTyped of string
exception WrongUriToConstant of string
exception WrongUriToVariable of string
exception WrongUriToMutualInductiveDefinitions of string
exception ListTooShort
exception RelToHiddenHypothesis

type types = {synthesized : Cic.term ; expected : Cic.term};;

module CicHash :
  sig
    type key = Cic.term
    and 'a t
    val find : 'a t -> key -> 'a
  end

val double_type_of :
 Cic.metasenv -> Cic.context -> Cic.term -> types CicHash.t