nasty change in the lexer/parser:

[helm.git] / helm / software / matita / library / R / Rexp.ma

diff --git a/helm/software/matita/library/R/Rexp.ma b/helm/software/matita/library/R/Rexp.ma
index 7cea392591ba9156589218480afed0bcc6d6e988..23b0c5cbb1927e4b278ed316bd3ed6d9d2999ad0 100644 (file)
--- a/helm/software/matita/library/R/Rexp.ma
+++ b/helm/software/matita/library/R/Rexp.ma
@@ -285,4 +285,4 @@ lemma aaa : ∀x,y:R.R1 < x → lub (expcut x y) (Rexp x y ?).
   |simplify;rewrite > H1 in H;elim (irrefl_Rlt ? H)]]
 qed.*)
 
-interpretation "real numbers exponent" 'exp a b = (Rexp a b _).
+interpretation "real numbers exponent" 'exp a b = (Rexp a b ?).