nasty change in the lexer/parser:

[helm.git] / helm / software / matita / library / dama / ordered_uniform.ma

diff --git a/helm/software/matita/library/dama/ordered_uniform.ma b/helm/software/matita/library/dama/ordered_uniform.ma
index 3485ae4c0e8bcb23efedc8475f561030ddea5918..6f72cd2449cf34b60ad1fc9619661ef5b1ed56fb 100644 (file)
--- a/helm/software/matita/library/dama/ordered_uniform.ma
+++ b/helm/software/matita/library/dama/ordered_uniform.ma
@@ -46,9 +46,9 @@ definition invert_os_relation ≝
   λC:ordered_set.λU:C squareO → Prop.
     λx:C squareO. U 〈\snd x,\fst x〉.
 
-interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
+interpretation "relation invertion" 'invert a = (invert_os_relation ? a).
+interpretation "relation invertion" 'invert_symbol = (invert_os_relation ?).
+interpretation "relation invertion" 'invert_appl a x = (invert_os_relation ? a x).
 
 lemma hint_segment: ∀O.
  segment (Type_of_ordered_set O) →
@@ -210,7 +210,7 @@ intros (O s); apply mk_ordered_uniform_space;
 qed.
 
 interpretation "Ordered uniform space segment" 'segset a = 
- (segment_ordered_uniform_space _ a).
+ (segment_ordered_uniform_space ? a).
 
 (* Lemma 3.2 *)
 alias symbol "pi1" = "exT \fst".