nasty change in the lexer/parser:

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

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index bc13ecfd7ee5ee6e259630e5a1a18a8c0de76a26..842219280ba10fcfe19eba1af70f08b4f8944197 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -200,7 +200,7 @@ qed.
 *)
 
 interpretation "lifting singl" 'singl x = 
- (fun11 _ (objs2 (POW _))  (singleton _) x).
+ (fun11 ? (objs2 (POW ?))  (singleton ?) x).
 
 theorem POW_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? POW S T g = f).
  intros; exists;