maction support added to notation, adopted for = AKA = \sub t

[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 4dec6442e0fd8e26ae995e3de4ef045968a014c1..f76660190d59476dca1d8bef9c1e0fb8bdc3e879 100644 (file)
--- a/helm/software/matita/library/dama/property_exhaustivity.ma
+++ b/helm/software/matita/library/dama/property_exhaustivity.ma
@@ -115,7 +115,7 @@ intros; split;
 qed.
 
 lemma hint_mah1:
-  ∀C. Type_OF_ordered_uniform_space1 C → hos_carr (os_r C).
+  ∀C. Type_OF_ordered_uniform_space__1 C → hos_carr (os_r C).
   intros; assumption; qed.
   
 coercion hint_mah1 nocomposites.