helm/gTopLevel/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 module CicHash :
  12   sig
  13     type 'a t
  14     val find : 'a t -> Cic.term -> 'a
  15   end
  16 ;;
  17
  18 val double_type_of :
  19  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t