From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Jul 2009 14:24:22 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3712
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1756fda18552874b063459b27448a4d0face1f39;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/topology/igt.ma b/helm/software/matita/nlibrary/topology/igt.ma
index fbe12b638..3dbdda6f0 100644
--- a/helm/software/matita/nlibrary/topology/igt.ma
+++ b/helm/software/matita/nlibrary/topology/igt.ma
@@ -27,21 +27,12 @@ nrecord setoid : Type[1] ≝
 ndefinition proofs: CProp → setoid.
 #P; napply (mk_setoid ?????);
 ##[ napply P;
-##|  napply (λ_,_.True);
-     #x; #y; napply True; (* DIVERGE *)
- intro;
- constructor 1;
-  [ apply A
-  | intros;
-    apply True
-  | intro;
-    constructor 1
-  | intros 3;
-    constructor 1
-  | intros 5;
-    constructor 1]
-qed.
+##| #x; #y; napply True;
+##|##*: nwhd; nrepeat (#_); napply I;
+##]
+nqed.
 
+(*
 definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
 definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
 definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
@@ -67,8 +58,10 @@ definition proofs1: CProp → setoid1.
   | intros 5;
     constructor 1]
 qed.
+*)
 
-definition CCProp: setoid1.
+(*
+ndefinition CCProp: setoid1.
  constructor 1;
   [ apply CProp
   | apply iff
@@ -88,17 +81,22 @@ definition CCProp: setoid1.
     | apply (H3 (H5 H))]]
 qed.
 
-record function_space (A,B: setoid): Type ≝
- { f:1> A → B;
+*)
+
+nrecord function_space (A,B: setoid): Type[1] ≝
+ { f:1> carr A → carr B}.;
    f_ok: ∀a,a':A. proofs (eq ? a a') → proofs (eq ? (f a) (f a'))
  }.
  
+
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 
+(*
 record function_space1 (A: setoid1) (B: setoid1): Type ≝
  { f1:1> A → B;
    f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a'))
  }.
+*)
 
 definition function_space_setoid: setoid → setoid → setoid.
  intros (A B);