Semantic analysis implemented (sort of).

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

diff --git a/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets2.ma b/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets2.ma
index 7e74cbba2a0b038d878a49d605b269dfd4a64157..b48c820a8a1c5357fccc2c09e19c1a7c8a1449b6 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets2.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/classical_pointfree/ordered_sets2.ma
@@ -61,7 +61,7 @@ theorem le_to_le_sup_sup:
 qed. 
 
 interpretation "mk_bounded_sequence" 'hide_everything_but a
-= (cic:/matita/classical_pointfree/ordered_sets/bounded_sequence.ind#xpointer(1/1/1) _ _ a _ _).
+= (mk_bounded_sequence _ _ a _ _).
 
 lemma reduce_bas_seq:
  ∀O:ordered_set.∀a:nat→O.∀p.∀i.