nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma
index 0d35ca981b8d864692376b0d6dd0e4bc6ab6a81b..8605105bf8e597c021761b0e45d3b7854ac268d3 100644 (file)
--- a/helm/software/matita/library/dama/property_exhaustivity.ma
+++ b/helm/software/matita/library/dama/property_exhaustivity.ma
@@ -28,8 +28,8 @@ qed.
 notation "'segment_upperbound'" non associative with precedence 90 for @{'segment_upperbound}.
 notation "'segment_lowerbound'" non associative with precedence 90 for @{'segment_lowerbound}.
 
-interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l _)).
-interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r _)).
+interpretation "segment_upperbound" 'segment_upperbound = (h_segment_upperbound (os_l ?)).
+interpretation "segment_lowerbound" 'segment_lowerbound = (h_segment_upperbound (os_r ?)).
 
 lemma h_segment_preserves_uparrow:
   ∀C:half_ordered_set.∀s:segment C.∀a:sequence (half_segment_ordered_set C s).
@@ -45,8 +45,8 @@ qed.
 notation "'segment_preserves_uparrow'" non associative with precedence 90 for @{'segment_preserves_uparrow}.
 notation "'segment_preserves_downarrow'" non associative with precedence 90 for @{'segment_preserves_downarrow}.
 
-interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l _)).
-interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r _)).
+interpretation "segment_preserves_uparrow" 'segment_preserves_uparrow = (h_segment_preserves_uparrow (os_l ?)).
+interpretation "segment_preserves_downarrow" 'segment_preserves_downarrow = (h_segment_preserves_uparrow (os_r ?)).
  
 (* Fact 2.18 *)
 lemma segment_cauchy:
@@ -90,8 +90,8 @@ qed.
 notation "'uparrow_to_in_segment'" non associative with precedence 90 for @{'uparrow_to_in_segment}.
 notation "'downarrow_to_in_segment'" non associative with precedence 90 for @{'downarrow_to_in_segment}.
 
-interpretation "uparrow_to_in_segment" 'uparrow_to_in_segment = (h_uparrow_to_in_segment (os_l _)).
-interpretation "downarrow_to_in_segment" 'downarrow_to_in_segment = (h_uparrow_to_in_segment (os_r _)).
+interpretation "uparrow_to_in_segment" 'uparrow_to_in_segment = (h_uparrow_to_in_segment (os_l ?)).
+interpretation "downarrow_to_in_segment" 'downarrow_to_in_segment = (h_uparrow_to_in_segment (os_r ?)).
  
 alias symbol "dependent_pair" = "dependent pair".
 (* Lemma 3.8 NON DUALIZZATO *)