X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Feqtype.ma;h=6aa3ff59fd2bf57600a558665606f7aa20e8b626;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=4c84e85ca1be5a2b1df1dc5fde5d74c7aa81de7d;hpb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma
index 4c84e85ca..6aa3ff59f 100644
--- a/helm/software/matita/library/decidable_kit/eqtype.ma
+++ b/helm/software/matita/library/decidable_kit/eqtype.ma
@@ -81,7 +81,7 @@ notation "{x, h}"
   right associative with precedence 80
 for @{'sig $x $h}.
 
-interpretation "sub_eqType" 'sig x h =  (mk_sigma _ _ x h).
+interpretation "sub_eqType" 'sig x h =  (mk_sigma ? ? x h).
 
 (* restricting an eqType gives an eqType *)
 lemma sigma_eq_dec : ∀d:eqType.∀p.∀x,y:sigma d p.