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