matitadep sould be ok, outputs warning regarding issues and

[helm.git] / matita / dama / classical_pointfree / ordered_sets.ma

diff --git a/matita/dama/classical_pointfree/ordered_sets.ma b/matita/dama/classical_pointfree/ordered_sets.ma
index 5d9c2da67132640b6d46720aaf9e8f34f5fd7488..2630da77c6474b93a99281982f1edc229ff27ae8 100644 (file)
--- a/matita/dama/classical_pointfree/ordered_sets.ma
+++ b/matita/dama/classical_pointfree/ordered_sets.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/classical_pointwise/ordered_sets/".
+
 
 include "excess.ma".
 
@@ -320,10 +320,10 @@ notation "hvbox(〈a〉)"
 for @{ 'hide_everything_but $a }.
 
 interpretation "mk_bounded_above_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 interpretation "mk_bounded_below_sequence" 'hide_everything_but a
-= (cic:/matita/ordered_set/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
 
 theorem eq_f_sup_sup_f:
  ∀O':dedekind_sigma_complete_ordered_set.