Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / tactics / FieldReflection.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/tactics/FieldReflection.mma b/helm/software/matita/contribs/CoRN-Procedural/tactics/FieldReflection.mma
index 91e5cd0fccf0834cd3c784a9d25ecdf1830972c3..dae6d36259f18c081d7dba795ec53ab166dfc398 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/tactics/FieldReflection.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/tactics/FieldReflection.mma
@@ -40,41 +40,41 @@ alias id "pfun" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Functi
 
 inline procedural "cic:/CoRN/tactics/FieldReflection/interpF.ind".
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/wfF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/wfF.con" as definition.
 
 inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF.ind".
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/xforgetF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xforgetF.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/xinterpF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xinterpF.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2interpF.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF_diagram_commutes.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/xexprF2wfF.con" as lemma.
 
 inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF.ind".
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_var.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_var.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_int.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_int.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_plus.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_plus.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_mult.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF_mult.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/fforgetF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fforgetF.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2interpF.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/fexprF2wfF.con" as lemma.
 
 include "tactics/Opaque_algebra.ma".
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/refl_interpF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/refl_interpF.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/interpF_wd.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/interpF_wd.con" as lemma.
 
 (* UNEXPORTED
 End Field_Interpretation_Function
@@ -116,7 +116,7 @@ P: sorted on M, all M's not an I
 Opaque Zmult.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/MI_mult_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Transparent Zmult.
@@ -126,7 +126,7 @@ Transparent Zmult.
 Opaque MI_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/MV_mult_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Transparent MI_mult.
@@ -136,7 +136,7 @@ Transparent MI_mult.
 Opaque MV_mult MI_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/MM_mult_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Transparent MV_mult MI_mult.
@@ -146,7 +146,7 @@ Transparent MV_mult MI_mult.
 Opaque MV_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/MM_plus_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Transparent MV_mult.
@@ -156,7 +156,7 @@ Transparent MV_mult.
 Opaque MM_plus.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/PM_plus_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Transparent MM_plus.
@@ -166,7 +166,7 @@ Transparent MM_plus.
 Opaque PM_plus.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/PP_plus_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Transparent PM_plus.
@@ -176,37 +176,37 @@ Transparent PM_plus.
 Opaque PM_plus MM_mult MI_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/PM_mult_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Opaque PM_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/PP_mult_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Transparent PP_plus PM_mult PP_mult PM_plus MI_mult.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/FF_plus_corr_F.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/FF_mult_corr_F.con" as lemma.
 
 (* UNEXPORTED
 Transparent FF_div.
 *)
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/FF_div_corr_F.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/NormF_corr.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/NormF_corr.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/Norm_wfF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/Norm_wfF.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/expr_is_zero_corr_F.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con".
+inline procedural "cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con" as lemma.
 
 (* UNEXPORTED
 End Field_NormCorrect