components/cic_acic/doubleTypeInference.mli

   1 exception Impossible of int
   2 exception NotWellTyped of string
   3 exception WrongUriToConstant of string
   4 exception WrongUriToVariable of string
   5 exception WrongUriToMutualInductiveDefinitions of string
   6 exception ListTooShort
   7 exception RelToHiddenHypothesis
   8
   9 type types = {synthesized : Cic.term ; expected : Cic.term option};;
  10
  11 val pack_coercion : (Cic.metasenv -> Cic.context -> Cic.term -> Cic.term) ref;;
  12
  13 val double_type_of :
  14  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
  15   types Cic.CicHash.t
  16
  17 (** Auxiliary functions **)
  18
  19 (* does_not_occur n te                              *)
  20 (* returns [true] if [Rel n] does not occur in [te] *)
  21 val does_not_occur : int -> Cic.term -> bool