(* $Id$ *)
val whd :
- ?delta:int -> ?subst:NCic.substitution ->
+ ?delta:int -> subst:NCic.substitution ->
NCic.context -> NCic.term ->
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