exception ListTooShort
exception RelToHiddenHypothesis
-type types = {synthesized : Cic.term ; expected : Cic.term};;
+type types = {synthesized : Cic.term ; expected : Cic.term option};;
module CicHash :
sig
- type key = Cic.term
- and 'a t
- val find : 'a t -> key -> 'a
+ type 'a t
+ val find : 'a t -> Cic.term -> 'a
end
+;;
val double_type_of :
- Cic.metasenv -> Cic.context -> Cic.term -> types CicHash.t
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
+
+(** Auxiliary functions **)
+
+(* does_not_occur n te *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+val does_not_occur : int -> Cic.term -> bool