X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FPartInterval.ma;h=a46add4bca731c3ee69e946037d162a062528fe4;hb=ee9a771a3cf2124ef65906ae75eb0ba7e2e4303b;hp=b4f8515cf5fc8f5307dd4cf9d624edf566d4cdc9;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
index b4f8515cf..a46add4bc 100644
--- a/helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
@@ -16,14 +16,14 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartInterval".
 
+include "CoRN.ma".
+
 (* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
 
-(* INCLUDE
-IntervalFunct
-*)
+include "ftc/IntervalFunct.ma".
 
 (* UNEXPORTED
-Section Conversion.
+Section Conversion
 *)
 
 (*#* *Correspondence
@@ -45,28 +45,28 @@ that [I [=] [a,b]] is included in the domain of [F].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/ftc/PartInterval/F.var.
+alias id "F" = "cic:/CoRN/ftc/PartInterval/Conversion/F.var".
 
-inline cic:/CoRN/ftc/PartInterval/a.var.
+alias id "a" = "cic:/CoRN/ftc/PartInterval/Conversion/a.var".
 
-inline cic:/CoRN/ftc/PartInterval/b.var.
+alias id "b" = "cic:/CoRN/ftc/PartInterval/Conversion/b.var".
 
-inline cic:/CoRN/ftc/PartInterval/Hab.var.
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Conversion/Hab.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/PartInterval/I.con.
+inline "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/PartInterval/Hf.var.
+alias id "Hf" = "cic:/CoRN/ftc/PartInterval/Conversion/Hf.var".
 
-inline cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con.
+inline "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con".
 
-inline cic:/CoRN/ftc/PartInterval/IntPartIR.con.
+inline "cic:/CoRN/ftc/PartInterval/IntPartIR.con".
 
 (* UNEXPORTED
-End Conversion.
+End Conversion
 *)
 
 (* UNEXPORTED
@@ -74,7 +74,7 @@ Implicit Arguments IntPartIR [F a b Hab].
 *)
 
 (* UNEXPORTED
-Section AntiConversion.
+Section AntiConversion
 *)
 
 (*#*
@@ -82,26 +82,26 @@ To go the other way around, we simply take a setoid function [f] with
 domain [[a,b]] and build the corresponding partial function.
 *)
 
-inline cic:/CoRN/ftc/PartInterval/a.var.
+alias id "a" = "cic:/CoRN/ftc/PartInterval/AntiConversion/a.var".
 
-inline cic:/CoRN/ftc/PartInterval/b.var.
+alias id "b" = "cic:/CoRN/ftc/PartInterval/AntiConversion/b.var".
 
-inline cic:/CoRN/ftc/PartInterval/Hab.var.
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/AntiConversion/Hab.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/PartInterval/I.con.
+inline "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/PartInterval/f.var.
+alias id "f" = "cic:/CoRN/ftc/PartInterval/AntiConversion/f.var".
 
-inline cic:/CoRN/ftc/PartInterval/PartInt_strext.con.
+inline "cic:/CoRN/ftc/PartInterval/PartInt_strext.con".
 
-inline cic:/CoRN/ftc/PartInterval/PartInt.con.
+inline "cic:/CoRN/ftc/PartInterval/PartInt.con".
 
 (* UNEXPORTED
-End AntiConversion.
+End AntiConversion
 *)
 
 (* UNEXPORTED
@@ -109,21 +109,21 @@ Implicit Arguments PartInt [a b Hab].
 *)
 
 (* UNEXPORTED
-Section Inverses.
+Section Inverses
 *)
 
 (*#*
 In one direction these operators are inverses.
 *)
 
-inline cic:/CoRN/ftc/PartInterval/int_part_int.con.
+inline "cic:/CoRN/ftc/PartInterval/int_part_int.con".
 
 (* UNEXPORTED
-End Inverses.
+End Inverses
 *)
 
 (* UNEXPORTED
-Section Equivalences.
+Section Equivalences
 *)
 
 (*#* **Mappings Preserve Operations
@@ -137,59 +137,59 @@ type [I->IR] equal respectively to [F] and [G] in [I].
 %\end{convention}%
 *)
 
-inline cic:/CoRN/ftc/PartInterval/F.var.
+alias id "F" = "cic:/CoRN/ftc/PartInterval/Equivalences/F.var".
 
-inline cic:/CoRN/ftc/PartInterval/G.var.
+alias id "G" = "cic:/CoRN/ftc/PartInterval/Equivalences/G.var".
 
-inline cic:/CoRN/ftc/PartInterval/a.var.
+alias id "a" = "cic:/CoRN/ftc/PartInterval/Equivalences/a.var".
 
-inline cic:/CoRN/ftc/PartInterval/b.var.
+alias id "b" = "cic:/CoRN/ftc/PartInterval/Equivalences/b.var".
 
-inline cic:/CoRN/ftc/PartInterval/c.var.
+alias id "c" = "cic:/CoRN/ftc/PartInterval/Equivalences/c.var".
 
-inline cic:/CoRN/ftc/PartInterval/Hab.var.
+alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hab.var".
 
 (* begin hide *)
 
-inline cic:/CoRN/ftc/PartInterval/I.con.
+inline "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__".
 
 (* end hide *)
 
-inline cic:/CoRN/ftc/PartInterval/f.var.
+alias id "f" = "cic:/CoRN/ftc/PartInterval/Equivalences/f.var".
 
-inline cic:/CoRN/ftc/PartInterval/g.var.
+alias id "g" = "cic:/CoRN/ftc/PartInterval/Equivalences/g.var".
 
-inline cic:/CoRN/ftc/PartInterval/Ff.var.
+alias id "Ff" = "cic:/CoRN/ftc/PartInterval/Equivalences/Ff.var".
 
-inline cic:/CoRN/ftc/PartInterval/Gg.var.
+alias id "Gg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Gg.var".
 
-inline cic:/CoRN/ftc/PartInterval/part_int_const.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_const.con".
 
-inline cic:/CoRN/ftc/PartInterval/part_int_id.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_id.con".
 
-inline cic:/CoRN/ftc/PartInterval/part_int_plus.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_plus.con".
 
-inline cic:/CoRN/ftc/PartInterval/part_int_inv.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_inv.con".
 
-inline cic:/CoRN/ftc/PartInterval/part_int_minus.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_minus.con".
 
-inline cic:/CoRN/ftc/PartInterval/part_int_mult.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_mult.con".
 
-inline cic:/CoRN/ftc/PartInterval/part_int_nth.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_nth.con".
 
 (* begin show *)
 
-inline cic:/CoRN/ftc/PartInterval/HG.var.
+alias id "HG" = "cic:/CoRN/ftc/PartInterval/Equivalences/HG.var".
 
-inline cic:/CoRN/ftc/PartInterval/Hg.var.
+alias id "Hg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hg.var".
 
 (* end show *)
 
-inline cic:/CoRN/ftc/PartInterval/part_int_recip.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_recip.con".
 
-inline cic:/CoRN/ftc/PartInterval/part_int_div.con.
+inline "cic:/CoRN/ftc/PartInterval/part_int_div.con".
 
 (* UNEXPORTED
-End Equivalences.
+End Equivalences
 *)