Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / algebra / Basics.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma b/helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma
index 598f294a1b03a5e6864376c23f59d77994f636f9..5e862ff9fa749223008dea9d99392bad18dc5b36 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/algebra/Basics.mma
@@ -42,26 +42,26 @@ include "algebra/ListType.ma".
 This is random stuff that should be in the Coq basic library.
 *)
 
-inline procedural "cic:/CoRN/algebra/Basics/lt_le_dec.con".
+inline procedural "cic:/CoRN/algebra/Basics/lt_le_dec.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/lt_z_two.con".
+inline procedural "cic:/CoRN/algebra/Basics/lt_z_two.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/le_pred.con".
+inline procedural "cic:/CoRN/algebra/Basics/le_pred.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/lt_mult_right.con".
+inline procedural "cic:/CoRN/algebra/Basics/lt_mult_right.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/le_mult_right.con".
+inline procedural "cic:/CoRN/algebra/Basics/le_mult_right.con" as lemma.
 
 (*#* The power function does not exist in the standard library *)
 
-inline procedural "cic:/CoRN/algebra/Basics/power.con".
+inline procedural "cic:/CoRN/algebra/Basics/power.con" as definition.
 
 (*#* Factorial function. Does not exist in Arith.
 Needed for special operations on polynomials. *)
 
-inline procedural "cic:/CoRN/algebra/Basics/fac.con".
+inline procedural "cic:/CoRN/algebra/Basics/fac.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con".
+inline procedural "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con" as lemma.
 
 (* needed for computational behavior of "Inversion" tactic *)
 
@@ -119,9 +119,9 @@ Intros. Right. Reflexivity.
 Qed.
 *)
 
-inline procedural "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con".
+inline procedural "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con".
+inline procedural "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con" as lemma.
 
 (* begin hide *)
 
@@ -148,31 +148,31 @@ cic:/Coq/ZArith/BinInt/Z_of_nat.con
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/algebra/Basics/POS_anti_convert.con".
+inline procedural "cic:/CoRN/algebra/Basics/POS_anti_convert.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/NEG_anti_convert.con".
+inline procedural "cic:/CoRN/algebra/Basics/NEG_anti_convert.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con".
+inline procedural "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con".
+inline procedural "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con".
+inline procedural "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/convert_is_POS.con".
+inline procedural "cic:/CoRN/algebra/Basics/convert_is_POS.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con".
+inline procedural "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/inject_nat_convert.con".
+inline procedural "cic:/CoRN/algebra/Basics/inject_nat_convert.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Z_exh.con".
+inline procedural "cic:/CoRN/algebra/Basics/Z_exh.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/nats_Z_ind.con".
+inline procedural "cic:/CoRN/algebra/Basics/nats_Z_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con".
+inline procedural "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con".
+inline procedural "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con".
+inline procedural "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con" as lemma.
 
 (* begin hide *)
 
@@ -186,7 +186,7 @@ Unset Strict Implicit.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff.con".
+inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff.con" as definition.
 
 (* begin hide *)
 
@@ -200,25 +200,25 @@ Unset Implicit Arguments.
 
 (* end hide *)
 
-inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_O.con".
+inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_O.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con".
+inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con".
+inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con".
+inline procedural "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/diff_Z_ind.con".
+inline procedural "cic:/CoRN/algebra/Basics/diff_Z_ind.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con".
+inline procedural "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Zlt_opp.con".
+inline procedural "cic:/CoRN/algebra/Basics/Zlt_opp.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con".
+inline procedural "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Zgt_not_eq.con".
+inline procedural "cic:/CoRN/algebra/Basics/Zgt_not_eq.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Zmult_absorb.con".
+inline procedural "cic:/CoRN/algebra/Basics/Zmult_absorb.con" as lemma.
 
 (* UNEXPORTED
 Section Well_foundedT
@@ -242,7 +242,7 @@ Section AccT
 
 alias id "A" = "cic:/CoRN/algebra/Basics/AccT/A.var".
 
-inline procedural "cic:/CoRN/algebra/Basics/well_founded.con".
+inline procedural "cic:/CoRN/algebra/Basics/well_founded.con" as definition.
 
 (* UNEXPORTED
 End AccT
@@ -268,9 +268,9 @@ alias id "P" = "cic:/CoRN/algebra/Basics/IndT/AccIter/P.var".
 
 alias id "F" = "cic:/CoRN/algebra/Basics/IndT/AccIter/F.var".
 
-inline procedural "cic:/CoRN/algebra/Basics/Acc_inv.con".
+inline procedural "cic:/CoRN/algebra/Basics/Acc_inv.con" as lemma.
 
-inline procedural "cic:/CoRN/algebra/Basics/Acc_iter.con".
+inline procedural "cic:/CoRN/algebra/Basics/Acc_iter.con" as definition.
 
 (* UNEXPORTED
 End AccIter
@@ -278,7 +278,7 @@ End AccIter
 
 alias id "Rwf" = "cic:/CoRN/algebra/Basics/IndT/Rwf.var".
 
-inline procedural "cic:/CoRN/algebra/Basics/well_founded_induction_type.con".
+inline procedural "cic:/CoRN/algebra/Basics/well_founded_induction_type.con" as theorem.
 
 (* UNEXPORTED
 End IndT
@@ -292,11 +292,11 @@ alias id "A" = "cic:/CoRN/algebra/Basics/InductionT/A.var".
 
 alias id "f" = "cic:/CoRN/algebra/Basics/InductionT/f.var".
 
-inline procedural "cic:/CoRN/algebra/Basics/ltof.con".
+inline procedural "cic:/CoRN/algebra/Basics/ltof.con" as definition.
 
-inline procedural "cic:/CoRN/algebra/Basics/well_founded_ltof.con".
+inline procedural "cic:/CoRN/algebra/Basics/well_founded_ltof.con" as theorem.
 
-inline procedural "cic:/CoRN/algebra/Basics/induction_ltof2T.con".
+inline procedural "cic:/CoRN/algebra/Basics/induction_ltof2T.con" as theorem.
 
 (* UNEXPORTED
 End InductionT
@@ -306,7 +306,7 @@ End InductionT
 Section InductionTT
 *)
 
-inline procedural "cic:/CoRN/algebra/Basics/lt_wf_rect.con".
+inline procedural "cic:/CoRN/algebra/Basics/lt_wf_rect.con" as lemma.
 
 (* UNEXPORTED
 End InductionTT