let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
NCic.Const ref
+;;
let set_default_eqP() = eqPref := default_eqP
let saturate t ty =
let sty, _, args =
- NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context
+ NCicMetaSubst.saturate ~delta:0 C.metasenv C.subst C.context
ty 0
in
let proof =