+let default_sig = function
+ | Eq ->
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+ let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
+ NCic.Const ref
+ | EqInd_l ->
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Def(1)) in
+ NCic.Const ref
+ | EqInd_r ->
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
+ NCic.Const ref
+ | Refl ->
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/peq.ind" in
+ let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
+ NCic.Const ref
+
+let set_default_sig () =
+ prerr_endline "setting default sig";
+ eqsig := default_sig
+
+let set_reference_of_oxuri reference_of_oxuri =
+ prerr_endline "setting oxuri in nCicProof";
+ let nsig = function
+ | Eq ->
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))
+ | EqInd_l ->
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_ind.con"))
+ | EqInd_r ->
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_elim_r.con"))
+ | Refl ->
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
+ in eqsig:= nsig