gran casino

[helm.git] / helm / software / matita / contribs / dama / dama / ordered_uniform.ma

diff --git a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
index 3bdfbe978f37a837f6aed589d7c46cac56aee8c5..1ca01611f66dd3b29e81269efc39ce640c2841e5 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_uniform.ma
@@ -86,8 +86,7 @@ lemma bs_of_ss:
  λO:ordered_set.λu,v:O.λb:{[u,v]} square.〈fst(fst b),fst(snd b)〉.
 
 notation < "x \sub \neq" non associative with precedence 91 for @{'bsss $x}.
-interpretation "bs_of_ss" 'bsss x = 
-  (cic:/matita/dama/ordered_uniform/bs_of_ss.con _ _ _ x).
+interpretation "bs_of_ss" 'bsss x = (bs_of_ss _ _ _ x).
 
 lemma segment_ordered_uniform_space: 
   ∀O:ordered_uniform_space.∀u,v:O.ordered_uniform_space.
@@ -135,7 +134,7 @@ intros (O l r); apply mk_ordered_uniform_space;
 qed.
 
 interpretation "Ordered uniform space segment" 'segment_set a b = 
- (cic:/matita/dama/ordered_uniform/segment_ordered_uniform_space.con _ a b).
+ (segment_ordered_uniform_space _ a b).
 
 (* Lemma 3.2 *)
 alias symbol "pi1" = "sigma pi1".