helm/ocaml/cic_omdoc/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 val syntactic_equality_add_time: float ref
  10 val type_of_aux'_add_time: float ref
  11 val number_new_type_of_aux'_double_work: int ref
  12 val number_new_type_of_aux': int ref
  13 val number_new_type_of_aux'_prop: int ref
  14
  15 type types = {synthesized : Cic.term ; expected : Cic.term option};;
  16
  17 module CicHash :
  18   sig
  19     type 'a t
  20     val find : 'a t -> Cic.term -> 'a
  21     val empty: unit -> 'a t
  22   end
  23 ;;
  24
  25 val double_type_of :
  26  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
  27
  28 (** Auxiliary functions **)
  29
  30 (* does_not_occur n te                              *)
  31 (* returns [true] if [Rel n] does not occur in [te] *)
  32 val does_not_occur : int -> Cic.term -> bool