X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fsigma.ma;h=e9c234eaf2a849a9e2b3703c456de9a716d1c00b;hb=11e495dda047bcdfa4267c06cad2d074fcffe3e3;hp=491d31e006113550d0904201c69978c7461df921;hpb=f2d9db85559c7a8db11aae1153495fae4a258d54;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/sigma.ma b/helm/software/matita/contribs/assembly/compiler/sigma.ma
index 491d31e00..e9c234eaf 100755
--- a/helm/software/matita/contribs/assembly/compiler/sigma.ma
+++ b/helm/software/matita/contribs/assembly/compiler/sigma.ma
@@ -39,9 +39,9 @@ notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
 
 notation "\ll term 19 a, break term 19 b \gg"
 with precedence 90 for @{'dependent_pair (λx:?.? x) $a $b}.
-interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro _ c a b).
+interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro ? c a b).
 
-interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
+interpretation "sigma" 'Sigma \eta.x = (sigma ? x).
 
 definition sigmaFst ≝
 λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].