X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FBasics.ma;h=32766572392cc0cc54d1dd59deeeeb53c06a8ca1;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=22f1f819a59b0df0de278501f96ed4580ec9b287;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/algebra/Basics.ma b/matita/contribs/CoRN-Decl/algebra/Basics.ma
index 22f1f819a..327665723 100644
--- a/matita/contribs/CoRN-Decl/algebra/Basics.ma
+++ b/matita/contribs/CoRN-Decl/algebra/Basics.ma
@@ -75,6 +75,18 @@ Transparent sym_eq.
 Transparent f_equal.
 *)
 
+(* NOTATION
+Notation Pair := (pair (B:=_)).
+*)
+
+(* NOTATION
+Notation Proj1 := (proj1 (B:=_)).
+*)
+
+(* NOTATION
+Notation Proj2 := (proj2 (B:=_)).
+*)
+
 (* Following only needed in finite, but tha's now obsolete
 
 Lemma deMorgan_or_and: (A,B,X:Prop)((A\/B)->X)->(A->X)/\(B->X).
@@ -132,7 +144,7 @@ coercion. *)
 
 (* begin hide *)
 
-coercion "cic:/matita/CoRN-Decl/algebra/Basics/Z_of_nat.con" 0 (* compounds *).
+coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *).
 
 (* end hide *)
 
@@ -209,31 +221,31 @@ inline "cic:/CoRN/algebra/Basics/Zgt_not_eq.con".
 inline "cic:/CoRN/algebra/Basics/Zmult_absorb.con".
 
 (* UNEXPORTED
-Section Well_foundedT.
+Section Well_foundedT
 *)
 
-inline "cic:/CoRN/algebra/Basics/A.var".
+alias id "A" = "cic:/CoRN/algebra/Basics/Well_foundedT/A.var".
 
-inline "cic:/CoRN/algebra/Basics/R.var".
+alias id "R" = "cic:/CoRN/algebra/Basics/Well_foundedT/R.var".
 
 (*#* The accessibility predicate is defined to be non-informative *)
 
 inline "cic:/CoRN/algebra/Basics/Acc.ind".
 
 (* UNEXPORTED
-End Well_foundedT.
+End Well_foundedT
 *)
 
 (* UNEXPORTED
-Section AccT.
+Section AccT
 *)
 
-inline "cic:/CoRN/algebra/Basics/A.var".
+alias id "A" = "cic:/CoRN/algebra/Basics/AccT/A.var".
 
 inline "cic:/CoRN/algebra/Basics/well_founded.con".
 
 (* UNEXPORTED
-End AccT.
+End AccT
 *)
 
 (* UNEXPORTED
@@ -241,44 +253,44 @@ Implicit Arguments Acc [A].
 *)
 
 (* UNEXPORTED
-Section IndT.
+Section IndT
 *)
 
-inline "cic:/CoRN/algebra/Basics/A.var".
+alias id "A" = "cic:/CoRN/algebra/Basics/IndT/A.var".
 
-inline "cic:/CoRN/algebra/Basics/R.var".
+alias id "R" = "cic:/CoRN/algebra/Basics/IndT/R.var".
 
 (* UNEXPORTED
-Section AccIter.
+Section AccIter
 *)
 
-inline "cic:/CoRN/algebra/Basics/P.var".
+alias id "P" = "cic:/CoRN/algebra/Basics/IndT/AccIter/P.var".
 
-inline "cic:/CoRN/algebra/Basics/F.var".
+alias id "F" = "cic:/CoRN/algebra/Basics/IndT/AccIter/F.var".
 
 inline "cic:/CoRN/algebra/Basics/Acc_inv.con".
 
 inline "cic:/CoRN/algebra/Basics/Acc_iter.con".
 
 (* UNEXPORTED
-End AccIter.
+End AccIter
 *)
 
-inline "cic:/CoRN/algebra/Basics/Rwf.var".
+alias id "Rwf" = "cic:/CoRN/algebra/Basics/IndT/Rwf.var".
 
 inline "cic:/CoRN/algebra/Basics/well_founded_induction_type.con".
 
 (* UNEXPORTED
-End IndT.
+End IndT
 *)
 
 (* UNEXPORTED
-Section InductionT.
+Section InductionT
 *)
 
-inline "cic:/CoRN/algebra/Basics/A.var".
+alias id "A" = "cic:/CoRN/algebra/Basics/InductionT/A.var".
 
-inline "cic:/CoRN/algebra/Basics/f.var".
+alias id "f" = "cic:/CoRN/algebra/Basics/InductionT/f.var".
 
 inline "cic:/CoRN/algebra/Basics/ltof.con".
 
@@ -287,16 +299,16 @@ inline "cic:/CoRN/algebra/Basics/well_founded_ltof.con".
 inline "cic:/CoRN/algebra/Basics/induction_ltof2T.con".
 
 (* UNEXPORTED
-End InductionT.
+End InductionT
 *)
 
 (* UNEXPORTED
-Section InductionTT.
+Section InductionTT
 *)
 
 inline "cic:/CoRN/algebra/Basics/lt_wf_rect.con".
 
 (* UNEXPORTED
-End InductionTT.
+End InductionTT
 *)