X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Fevars.cic;h=36ce17e2efac85d8f77bdef6fed38bf64e8f51be;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=9183cb1e4a22594b067b5537a45dcc66607d0905;hpb=fde1a6daa3aaa72c5c7536f4d2c65a3873b1c1bc;p=helm.git

diff --git a/helm/gTopLevel/esempi/evars.cic b/helm/gTopLevel/esempi/evars.cic
index 9183cb1e4..36ce17e2e 100644
--- a/helm/gTopLevel/esempi/evars.cic
+++ b/helm/gTopLevel/esempi/evars.cic
@@ -1,9 +1,9 @@
 alias nat          /Coq/Init/Datatypes/nat.ind#1/1
 alias eqT          /Coq/Init/Logic_Type/eqT.ind#1/1
-alias eq           /Coq/Init/Logic/Equality/eq.ind#1/1
-alias refl_equal   /Coq/Init/Logic/Equality/eq.ind#1/1/1
-alias eq_ind       /Coq/Init/Logic/Equality/eq_ind.con
-alias eq_ind_r     /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con
+alias eq           /Coq/Init/Logic/eq.ind#1/1
+alias refl_equal   /Coq/Init/Logic/eq.ind#1/1/1
+alias eq_ind       /Coq/Init/Logic/eq_ind.con
+alias eq_ind_r     /Coq/Init/Logic/eq_ind_r.con
 alias O            /Coq/Init/Datatypes/nat.ind#1/1/1
 alias S            /Coq/Init/Datatypes/nat.ind#1/1/2
 alias plus         /Coq/Init/Peano/plus.con
@@ -11,7 +11,7 @@ alias mult         /Coq/Init/Peano/mult.con
 alias le           /Coq/Init/Peano/le.ind#1/1
 alias lt           /Coq/Init/Peano/lt.con
 alias not          /Coq/Init/Logic/not.con
-alias f_equal      /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con
+alias f_equal      /Coq/Init/Logic/f_equal.con
 alias le_trans     /Coq/Arith/Le/le_trans.con
 
 alias le_plus_plus /Coq/Arith/Plus/le_plus_plus.con