- transcript: bugfix

[helm.git] / helm / software / matita / library / decidable_kit / eqtype.ma

diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma
index fe3964c65dd647dd0b3575b31941cf593c2e355f..4c84e85ca1be5a2b1df1dc5fde5d74c7aa81de7d 100644 (file)
--- a/helm/software/matita/library/decidable_kit/eqtype.ma
+++ b/helm/software/matita/library/decidable_kit/eqtype.ma
@@ -81,8 +81,7 @@ notation "{x, h}"
   right associative with precedence 80
 for @{'sig $x $h}.
 
-interpretation "sub_eqType" 'sig x h = 
-  (cic:/matita/decidable_kit/eqtype/sigma.ind#xpointer(1/1/1) _ _ 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.