X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fclassical_pointfree%2Fordered_sets.ma;h=280f409cfedbd1a61b262fa98c702668bde49b2a;hb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;hp=2630da77c6474b93a99281982f1edc229ff27ae8;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets.ma b/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets.ma
index 2630da77c..280f409cf 100644
--- a/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets.ma
@@ -320,10 +320,10 @@ notation "hvbox(〈a〉)"
 for @{ 'hide_everything_but $a }.
 
 interpretation "mk_bounded_above_sequence" 'hide_everything_but a
-= (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (mk_bounded_above_sequence _ _ a _).
 
 interpretation "mk_bounded_below_sequence" 'hide_everything_but a
-= (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (mk_bounded_below_sequence _ _ a _).
 
 theorem eq_f_sup_sup_f:
  ∀O':dedekind_sigma_complete_ordered_set.