nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / dama / dama_duality / metric_space.ma

diff --git a/helm/software/matita/contribs/dama/dama_duality/metric_space.ma b/helm/software/matita/contribs/dama/dama_duality/metric_space.ma
index cda8d3fc757c711c9e6f6bda03064342b3f41d86..7d91a68e82c0b4567320628eca13aa8d61af7a4d 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/metric_space.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/metric_space.ma
@@ -24,9 +24,9 @@ record metric_space (R: todgroup) : Type ≝ {
 }.
 
 notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}.
-interpretation "metric" 'delta2 a b = (metric _ _ a b).
+interpretation "metric" 'delta2 a b = (metric ? ? a b).
 notation "\delta" non associative with precedence 80 for @{ 'delta }.
-interpretation "metric" 'delta = (metric _ _).
+interpretation "metric" 'delta = (metric ? ?).
 
 lemma apart_of_metric_space: ∀R.metric_space R → apartness.
 intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold;