* For details, see the HELM World-Wide-Web page,
* http://helm.cs.unibo.it/
*)
+
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 * 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
+val is_meta_closed : Cic.term -> bool
+
+val term_of_uri: string -> Cic.term