nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / dama / dama / models / q_bars.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/q_bars.ma b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
index f3224e627efb5f35c27a129b0dc88396bfeaa19c..2cad9ca2add1adbdb9efa018723ee99809c4b99f 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_bars.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_bars.ma
@@ -31,7 +31,7 @@ interpretation "lq2" 'lq2 = (list bar).
 
 definition q2_lt := mk_rel bar (λx,y:bar.\fst x < \fst y).
 
-interpretation "bar lt" 'lt x y = (rel_op _ q2_lt x y).
+interpretation "bar lt" 'lt x y = (rel_op ? q2_lt x y).
 
 lemma q2_trans : ∀a,b,c:bar. a < b → b < c → a < c.
 intros 3; cases a; cases b; cases c; unfold q2_lt; simplify; intros;
@@ -46,7 +46,7 @@ definition canonical_q_lt : rel bar → trans_rel ≝ λx:rel bar.q2_trel.
 
 coercion canonical_q_lt with nocomposites.
 
-interpretation "bar lt" 'lt x y = (FunClass_2_OF_trans_rel (canonical_q_lt _) x y).
+interpretation "bar lt" 'lt x y = (FunClass_2_OF_trans_rel (canonical_q_lt ?) x y).
 
 definition nth_base ≝ λf,n. \fst (\nth f ▭ n).
 definition nth_height ≝ λf,n. \snd (\nth f ▭ n).
@@ -197,5 +197,5 @@ cases (?:False);
 qed.
 
 notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}.
-interpretation "hide unpos proof" 'unpos x = (unpos x _).
+interpretation "hide unpos proof" 'unpos x = (unpos x ?).