(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-val mk_proof:
- NCic.term Terms.bag -> Terms.M.key -> Terms.M.key list -> NCic.term
+type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
+val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
+val set_default_sig: unit -> unit
+val get_sig: eq_sig_type -> NCic.term
+val mk_proof:
+ NCic.term Terms.bag
+ -> Terms.M.key
+ -> NCic.term Terms.substitution
+ -> Terms.M.key list
+ -> NCic.term * NCic.term (* proof, type *)