- transcript: patched to generate aliases instead of inlined variables

[helm.git] / matita / contribs / CoRN-Decl / ftc / PartInterval.ma

diff --git a/matita/contribs/CoRN-Decl/ftc/PartInterval.ma b/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
index 47e16466381868b19a084c22cac77b04f7f01c4f..a46add4bca731c3ee69e946037d162a062528fe4 100644 (file)
--- a/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
+++ b/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
@@ -23,7 +23,7 @@ include "CoRN.ma".
 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.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.con".
 
 (* UNEXPORTED
-End AntiConversion.
+End AntiConversion
 *)
 
 (* UNEXPORTED
@@ -109,7 +109,7 @@ Implicit Arguments PartInt [a b Hab].
 *)
 
 (* UNEXPORTED
-Section Inverses.
+Section Inverses
 *)
 
 (*#*
@@ -119,11 +119,11 @@ In one direction these operators are inverses.
 inline "cic:/CoRN/ftc/PartInterval/int_part_int.con".
 
 (* UNEXPORTED
-End Inverses.
+End Inverses
 *)
 
 (* UNEXPORTED
-Section Equivalences.
+Section Equivalences
 *)
 
 (*#* **Mappings Preserve Operations
@@ -137,31 +137,31 @@ 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".
 
@@ -179,9 +179,9 @@ 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 *)
 
@@ -190,6 +190,6 @@ inline "cic:/CoRN/ftc/PartInterval/part_int_recip.con".
 inline "cic:/CoRN/ftc/PartInterval/part_int_div.con".
 
 (* UNEXPORTED
-End Equivalences.
+End Equivalences
 *)