the new coercion behaviour (variants + composition with ID) and the new

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / saturations_to_o-saturations.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
index ce6c6f110ac571e7483bd9d51151eac80974783b..97bfcd6c9d19aac7ea9c591209479db41d5fbc13 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
@@ -20,7 +20,7 @@ include "relations_to_o-algebra.ma".
 
 definition o_operator_of_operator:
  ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C).
- intros;apply t;
+ intros (C t);apply t;
 qed.
 
 definition is_o_saturation_of_is_saturation: