Yet another universe problem :-(

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-algebra.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index c6d91db945e94a04e325b2d33751e26022142a22..55d692190fdae75667e0efdcb678d83e087b84c3 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -134,9 +134,7 @@ intros; split;
   intro x; simplify; cases x; simplify; assumption;]
 qed.
 
-notation "hovbox(a ∧ b)" left associative with precedence 35
-for @{ 'oa_meet_bin $a $b }.
-interpretation "o-algebra binary meet" 'oa_meet_bin a b = 
+interpretation "o-algebra binary meet" 'and a b = 
   (fun21 ___ (binary_meet _) a b).
 
 coercion Type1_OF_OAlgebra nocomposites.
@@ -349,4 +347,4 @@ coercion objs2_SET1_OF_OA.
 lemma Type_OF_category2_OF_SET1_OF_OA: OA → Type_OF_category2 SET1.
  intro; apply (oa_P t);
 qed.
-coercion Type_OF_category2_OF_SET1_OF_OA.
\ No newline at end of file
+coercion Type_OF_category2_OF_SET1_OF_OA.