+++ /dev/null
-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 option};;
-
-module CicHash :
- sig
- type 'a t
- val find : 'a t -> Cic.term -> 'a
- end
-;;
-
-val double_type_of :
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t