X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_didactic%2Fbottom.ma;h=08c1b976136ef3fcba94ce955d389f7b89a4e893;hb=38fccc2b774e493a94eedef76342b56079c0e694;hp=161063b426341ca18c2c8d6b6723287f35749d1f;hpb=d4302f43737034a69bd475e5f46e8d126229375e;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_didactic/bottom.ma b/helm/software/matita/contribs/dama/dama_didactic/bottom.ma
index 161063b42..08c1b9761 100644
--- a/helm/software/matita/contribs/dama/dama_didactic/bottom.ma
+++ b/helm/software/matita/contribs/dama/dama_didactic/bottom.ma
@@ -30,8 +30,7 @@ notation "hvbox(a break ≡ b)"
   non associative with precedence 45
 for @{ 'equiv $a $b }.
 
-interpretation "uguaglianza parziale" 'equiv x y =
- (cic:/matita/tests/decl/eq.ind#xpointer(1/1) _ x y).
+interpretation "uguaglianza parziale" 'equiv x y = (eq ? x y).
 
 coercion cic:/matita/tests/decl/L.ind#xpointer(1/1/2).
  
@@ -62,14 +61,11 @@ axiom Relev: L R→L R→L R.
 axiom Rle: L R→L R→Prop.
 axiom Rge: L R→L R→Prop.
 
-interpretation "real plus" 'plus x y =
- (cic:/matita/tests/decl/Rplus.con x y).
+interpretation "real plus" 'plus x y = (Rplus x y).
 
-interpretation "real leq" 'leq x y =
- (cic:/matita/tests/decl/Rle.con x y).
+interpretation "real leq" 'leq x y = (Rle x y).
 
-interpretation "real geq" 'geq x y =
- (cic:/matita/tests/decl/Rge.con x y).
+interpretation "real geq" 'geq x y = (Rge x y).
 
 let rec elev (x:L R) (n:nat) on n: L R ≝
  match n with