]> matita.cs.unibo.it Git - helm.git/commitdiff
Wrong reference corrected
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 9 Dec 2009 15:48:41 +0000 (15:48 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 9 Dec 2009 15:48:41 +0000 (15:48 +0000)
helm/software/components/ng_paramodulation/nCicProof.ml

index 28c6f9e038d48f4ac12645ed53b390cf258666f6..59d7e95ff65f824b0e70b968aa4b16d1ecbb9aec 100644 (file)
@@ -29,7 +29,7 @@ let default_sig = function
        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(2)) 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