a) update with upstream version

[helm.git] / helm / software / matita / contribs / dama / dama_duality / classical_pointfree / ordered_sets.ma

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 2630da77c6474b93a99281982f1edc229ff27ae8..280f409cfedbd1a61b262fa98c702668bde49b2a 100644 (file)
--- 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.