(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-module NCicParamod(C : NCicBlob.NCicContext) : Paramod.Paramod
-with type t = NCic.term and type input = NCic.term
-
val nparamod :
#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
+val forward_infer_step: state -> NCic.term -> NCic.term -> state
+val index_obj: state -> NUri.uri -> state
+val is_equation: NCic.metasenv ->
+ NCic.substitution -> NCic.context -> NCic.term -> bool
+val paramod :
+ #NRstatus.status ->
+ NCic.metasenv -> NCic.substitution -> NCic.context ->
+ state ->
+ (NCic.term * NCic.term) ->
+ (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
+val fast_eq_check :
+ #NRstatus.status ->
+ NCic.metasenv -> NCic.substitution -> NCic.context ->
+ state ->
+ (NCic.term * NCic.term) ->
+ (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list