*)
exception Meta_not_found of int
+exception Subst_not_found of int
val lookup_meta: int -> Cic.metasenv -> Cic.conjecture
+val lookup_subst: int -> Cic.substitution -> Cic.context * Cic.term
val exists_meta: int -> Cic.metasenv -> bool
+val clean_up_local_context :
+ Cic.substitution -> Cic.metasenv -> int -> (Cic.term option) list
+ -> (Cic.term option) list
val is_closed : Cic.term -> bool