X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fproperty_exhaustivity.ma;h=f76660190d59476dca1d8bef9c1e0fb8bdc3e879;hb=8d961585c4ff785d558d5b4c84adf656595ca487;hp=4dec6442e0fd8e26ae995e3de4ef045968a014c1;hpb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;p=helm.git

diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma
index 4dec6442e..f76660190 100644
--- 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.