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 4c84e85ca1be5a2b1df1dc5fde5d74c7aa81de7d..6aa3ff59fd2bf57600a558665606f7aa20e8b626 100644 (file)
--- 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.