From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 Dec 2008 18:12:47 +0000 (+0000)
Subject: Some fixes.
X-Git-Tag: make_still_working~4321
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6454e0578b1b3b3bb7c9f9a60946e1a4c2f97ff3;p=helm.git

Some fixes.
---

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
index 5b08b5917..9cbaada80 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
@@ -47,7 +47,8 @@ lemma xxx : ∀x.carr x → carr1 (setoid1_of_setoid x). intros; assumption; qed
 coercion xxx nocomposites.
 
 lemma down_p : ∀S,I:SET.∀u:S⇒S.∀c:arrows1 SET I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a').
-intros; unfold uncurry_arrows; apply (†(†H));
+intros; unfold uncurry_arrows; change in c with (I ⇒ S);
+apply (†(†H));
 qed.
 
 alias symbol "eq" = "setoid eq".
@@ -122,7 +123,7 @@ definition convergent_relation_space_composition:
  ∀o1,o2,o3: concrete_space.
   binary_morphism1
    (convergent_relation_space_setoid o1 o2)
-   (convergentin ⊢ (? (? ? ? (? ? ? (? ? ? ? ? (? ? ? (? ? ? (% ? ?))) ?)) ?) ? ? ?)_relation_space_setoid o2 o3)
+   (convergent_relation_space_setoid o2 o3)
    (convergent_relation_space_setoid o1 o3).
  intros; constructor 1;
      [ intros; whd in c c1 ⊢ %;