ocaml 3.09 transition

[helm.git] / helm / gTopLevel / esempi / evars.cic

diff --git a/helm/gTopLevel/esempi/evars.cic b/helm/gTopLevel/esempi/evars.cic
index 9183cb1e4a22594b067b5537a45dcc66607d0905..36ce17e2efac85d8f77bdef6fed38bf64e8f51be 100644 (file)
--- 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