freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / CoRN-Decl / algebra / Basics.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma
index 8794b52cc732184ca9aa34ed827c8b4fb2d37a54..32766572392cc0cc54d1dd59deeeeb53c06a8ca1 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics".
 
+include "CoRN.ma".
+
 (* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *)
 
 (*#* printing alpha %\ensuremath{\alpha}% #α# *)
@@ -36,50 +38,32 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics".
 
 (*#* printing Z %\ensuremath{\mathbb Z}% #<b>Z</b># *)
 
-(* INCLUDE
-Omega
-*)
-
-(* INCLUDE
-Even
-*)
-
-(* INCLUDE
-Max
-*)
-
-(* INCLUDE
-Min
-*)
-
-(* INCLUDE
-ListType
-*)
+include "algebra/ListType.ma".
 
 (*#* *Basics
 This is random stuff that should be in the Coq basic library.
 *)
 
-inline cic:/CoRN/algebra/Basics/lt_le_dec.con.
+inline "cic:/CoRN/algebra/Basics/lt_le_dec.con".
 
-inline cic:/CoRN/algebra/Basics/lt_z_two.con.
+inline "cic:/CoRN/algebra/Basics/lt_z_two.con".
 
-inline cic:/CoRN/algebra/Basics/le_pred.con.
+inline "cic:/CoRN/algebra/Basics/le_pred.con".
 
-inline cic:/CoRN/algebra/Basics/lt_mult_right.con.
+inline "cic:/CoRN/algebra/Basics/lt_mult_right.con".
 
-inline cic:/CoRN/algebra/Basics/le_mult_right.con.
+inline "cic:/CoRN/algebra/Basics/le_mult_right.con".
 
 (*#* The power function does not exist in the standard library *)
 
-inline cic:/CoRN/algebra/Basics/power.con.
+inline "cic:/CoRN/algebra/Basics/power.con".
 
 (*#* Factorial function. Does not exist in Arith.
 Needed for special operations on polynomials. *)
 
-inline cic:/CoRN/algebra/Basics/fac.con.
+inline "cic:/CoRN/algebra/Basics/fac.con".
 
-inline cic:/CoRN/algebra/Basics/nat_fac_gtzero.con.
+inline "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con".
 
 (* needed for computational behavior of "Inversion" tactic *)
 
@@ -91,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).
@@ -125,9 +121,9 @@ Intros. Right. Reflexivity.
 Qed.
 *)
 
-inline cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con.
+inline "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con".
 
-inline cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con.
+inline "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con".
 
 (* begin hide *)
 
@@ -148,33 +144,35 @@ coercion. *)
 
 (* begin hide *)
 
+coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *).
+
 (* end hide *)
 
-inline cic:/CoRN/algebra/Basics/POS_anti_convert.con.
+inline "cic:/CoRN/algebra/Basics/POS_anti_convert.con".
 
-inline cic:/CoRN/algebra/Basics/NEG_anti_convert.con.
+inline "cic:/CoRN/algebra/Basics/NEG_anti_convert.con".
 
-inline cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con.
+inline "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con".
 
-inline cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con.
+inline "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con".
 
-inline cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con.
+inline "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con".
 
-inline cic:/CoRN/algebra/Basics/convert_is_POS.con.
+inline "cic:/CoRN/algebra/Basics/convert_is_POS.con".
 
-inline cic:/CoRN/algebra/Basics/min_convert_is_NEG.con.
+inline "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con".
 
-inline cic:/CoRN/algebra/Basics/inject_nat_convert.con.
+inline "cic:/CoRN/algebra/Basics/inject_nat_convert.con".
 
-inline cic:/CoRN/algebra/Basics/Z_exh.con.
+inline "cic:/CoRN/algebra/Basics/Z_exh.con".
 
-inline cic:/CoRN/algebra/Basics/nats_Z_ind.con.
+inline "cic:/CoRN/algebra/Basics/nats_Z_ind.con".
 
-inline cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con.
+inline "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con".
 
-inline cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con.
+inline "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con".
 
-inline cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con.
+inline "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con".
 
 (* begin hide *)
 
@@ -188,7 +186,7 @@ Unset Strict Implicit.
 
 (* end hide *)
 
-inline cic:/CoRN/algebra/Basics/caseZ_diff.con.
+inline "cic:/CoRN/algebra/Basics/caseZ_diff.con".
 
 (* begin hide *)
 
@@ -202,52 +200,52 @@ Unset Implicit Arguments.
 
 (* end hide *)
 
-inline cic:/CoRN/algebra/Basics/caseZ_diff_O.con.
+inline "cic:/CoRN/algebra/Basics/caseZ_diff_O.con".
 
-inline cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con.
+inline "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con".
 
-inline cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con.
+inline "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con".
 
-inline cic:/CoRN/algebra/Basics/proper_caseZ_diff.con.
+inline "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con".
 
-inline cic:/CoRN/algebra/Basics/diff_Z_ind.con.
+inline "cic:/CoRN/algebra/Basics/diff_Z_ind.con".
 
-inline cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con.
+inline "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con".
 
-inline cic:/CoRN/algebra/Basics/Zlt_opp.con.
+inline "cic:/CoRN/algebra/Basics/Zlt_opp.con".
 
-inline cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con.
+inline "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con".
 
-inline cic:/CoRN/algebra/Basics/Zgt_not_eq.con.
+inline "cic:/CoRN/algebra/Basics/Zgt_not_eq.con".
 
-inline cic:/CoRN/algebra/Basics/Zmult_absorb.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.
+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.
+inline "cic:/CoRN/algebra/Basics/well_founded.con".
 
 (* UNEXPORTED
-End AccT.
+End AccT
 *)
 
 (* UNEXPORTED
@@ -255,62 +253,62 @@ 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_inv.con".
 
-inline cic:/CoRN/algebra/Basics/Acc_iter.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.
+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.
+inline "cic:/CoRN/algebra/Basics/ltof.con".
 
-inline cic:/CoRN/algebra/Basics/well_founded_ltof.con.
+inline "cic:/CoRN/algebra/Basics/well_founded_ltof.con".
 
-inline cic:/CoRN/algebra/Basics/induction_ltof2T.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.
+inline "cic:/CoRN/algebra/Basics/lt_wf_rect.con".
 
 (* UNEXPORTED
-End InductionTT.
+End InductionTT
 *)