]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/esempi/prova.cic
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / esempi / prova.cic
index 6ca06a8620a3b1adc4899ea77a8f7baaa6720fe3..3f65458d25847666c6f2f96e2ae72383b6266de3 100644 (file)
@@ -1,4 +1,4 @@
-alias eq   /Coq/Init/Logic/Equality/eq.ind#1/1
+alias eq   /Coq/Init/Logic/eq.ind#1/1
 alias nat  /Coq/Init/Datatypes/nat.ind#1/1
 alias O    /Coq/Init/Datatypes/nat.ind#1/1/1
 alias S    /Coq/Init/Datatypes/nat.ind#1/1/2