type types = {synthesized : Cic.term ; expected : Cic.term option};;
-module CicHash :
- sig
- type 'a t
- val find : 'a t -> Cic.term -> 'a
- val empty: unit -> 'a t
- end
-;;
-
val double_type_of :
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option ->
+ types Cic.CicHash.t
(** Auxiliary functions **)