val set_eqP: NCic.term -> unit
val set_default_eqP: unit -> unit
+val saturate:
+ #NCicEnvironment.status ->
+ NCic.metasenv ->
+ NCic.substitution ->
+ NCic.context -> NCic.term -> NCic.term -> NCic.term * NCic.term
+(*
module type NCicContext =
sig
val metasenv : NCic.metasenv
val subst : NCic.substitution
val context : NCic.context
end
+*)
-module NCicBlob(C : NCicContext) : Terms.Blob
+module NCicBlob: Terms.Blob
with type t = NCic.term and type input = NCic.term