X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fextra.ma;h=008d84202c8b759211aae7906df041056b78491e;hb=9eabe046c1182960de8cfdba96c5414224e3a61e;hp=d36e0db7e165d9e1be7aeb1f827b4fc43959999a;hpb=648db01678fac09ddfb3cce900bc72e8a1c420da;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/extra.ma b/helm/software/matita/contribs/dama/dama/extra.ma
index d36e0db7e..008d84202 100644
--- a/helm/software/matita/contribs/dama/dama/extra.ma
+++ b/helm/software/matita/contribs/dama/dama/extra.ma
@@ -20,7 +20,7 @@ definition strong_ext ≝ λA:bishop_set.λop:A→A.∀x,y. op x # op y → x #
 
 definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b.
 
-interpretation "ordered sets less than" 'lt a b = (cic:/matita/dama/excess/lt.con _ a b).
+interpretation "ordered sets less than" 'lt a b = (lt _ a b).
 
 lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
 intros 2 (E x); intro H; cases H (_ ABS); 
@@ -51,9 +51,9 @@ intros (A x y z E H); split; cases H;
 qed.
 
 notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}.
-interpretation "lt_rewl" 'ltrewritel = (cic:/matita/dama/excess/lt_rewl.con _ _ _).
+interpretation "lt_rewl" 'ltrewritel = (lt_rewl _ _ _).
 notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}.
-interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/excess/lt_rewr.con _ _ _).
+interpretation "lt_rewr" 'ltrewriter = (lt_rewr _ _ _).
 
 lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z.
 intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]