+
+val get_clears:
+ Cic.context -> Cic.term -> (Cic.term * Cic.term) option ->
+ Cic.context * string list
+
+val clear: Cic.context -> string -> Cic.context
+
+val elim_inferred_type:
+ Cic.context -> Cic.term -> Cic.term -> Cic.term -> Cic.term -> Cic.term