+val set_get_relevance :
+ (metasenv:NCic.metasenv -> subst:NCic.substitution ->
+ NCic.context -> NCic.term -> NCic.term list -> bool list) -> unit
+
+val are_convertible :
+ metasenv:NCic.metasenv -> subst:NCic.substitution ->
+ NCic.context -> NCic.term -> NCic.term -> bool
+