minor changes to make the library compile after wilmers new exists.

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

diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma
index be8495970a737e9f926066f381c134b7a9784dd0..2ce417ecce9398a7e9405ce347ae65ff15772718 100644 (file)
--- a/helm/software/matita/library/dama/supremum.ma
+++ b/helm/software/matita/library/dama/supremum.ma
@@ -121,7 +121,7 @@ interpretation "trans_increasing" 'trans_increasing = (h_trans_increasing (os_l
 interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
 
 lemma hint_nat :
- Type_of_ordered_set nat_ordered_set →
+ Type_OF_ordered_set nat_ordered_set →
    hos_carr (os_l (nat_ordered_set)).
 intros; assumption;
 qed.