#NRstatus.status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
(NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
- (NCic.term * NCic.metasenv * NCic.substitution) list
+ (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
type state
val empty_state: state
NCic.metasenv -> NCic.substitution -> NCic.context ->
state ->
(NCic.term * NCic.term) ->
- (NCic.term * NCic.metasenv * NCic.substitution) list
+ (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list