nasty change in the lexer/parser:

[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..6aa3ff59fd2bf57600a558665606f7aa20e8b626 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.