freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / CoRN-Decl / tactics / RingReflection.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma b/helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
index bd88498502e23bed029a7d995898f307d03d4844..84a076ad99d28cb5c0ebe3eab29cfdbf71a3db6d 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
@@ -16,63 +16,61 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/tactics/RingReflection".
 
+include "CoRN.ma".
+
 (* $Id: RingReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
 
 (* begin hide *)
 
-(* INCLUDE
-CRings
-*)
+include "algebra/CRings.ma".
 
-(* INCLUDE
-AlgReflection
-*)
+include "tactics/AlgReflection.ma".
 
 (* UNEXPORTED
-Section Ring_Interpretation_Function.
+Section Ring_Interpretation_Function
 *)
 
-inline cic:/CoRN/tactics/RingReflection/R.var.
+alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/R.var".
 
-inline cic:/CoRN/tactics/RingReflection/val.var.
+alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/val.var".
 
-inline cic:/CoRN/tactics/RingReflection/unop.var.
+alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/unop.var".
 
-inline cic:/CoRN/tactics/RingReflection/binop.var.
+alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/binop.var".
 
-inline cic:/CoRN/tactics/RingReflection/pfun.var.
+alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/pfun.var".
 
-inline cic:/CoRN/tactics/RingReflection/interpR.ind.
+inline "cic:/CoRN/tactics/RingReflection/interpR.ind".
 
-inline cic:/CoRN/tactics/RingReflection/wfR.con.
+inline "cic:/CoRN/tactics/RingReflection/wfR.con".
 
-inline cic:/CoRN/tactics/RingReflection/xexprR.ind.
+inline "cic:/CoRN/tactics/RingReflection/xexprR.ind".
 
-inline cic:/CoRN/tactics/RingReflection/xforgetR.con.
+inline "cic:/CoRN/tactics/RingReflection/xforgetR.con".
 
-inline cic:/CoRN/tactics/RingReflection/xinterpR.con.
+inline "cic:/CoRN/tactics/RingReflection/xinterpR.con".
 
-inline cic:/CoRN/tactics/RingReflection/xexprR2interpR.con.
+inline "cic:/CoRN/tactics/RingReflection/xexprR2interpR.con".
 
-inline cic:/CoRN/tactics/RingReflection/xexprR_diagram_commutes.con.
+inline "cic:/CoRN/tactics/RingReflection/xexprR_diagram_commutes.con".
 
-inline cic:/CoRN/tactics/RingReflection/xexprR2wfR.con.
+inline "cic:/CoRN/tactics/RingReflection/xexprR2wfR.con".
 
-inline cic:/CoRN/tactics/RingReflection/fexprR.ind.
+inline "cic:/CoRN/tactics/RingReflection/fexprR.ind".
 
-inline cic:/CoRN/tactics/RingReflection/fexprR_var.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR_var.con".
 
-inline cic:/CoRN/tactics/RingReflection/fexprR_int.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR_int.con".
 
-inline cic:/CoRN/tactics/RingReflection/fexprR_plus.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR_plus.con".
 
-inline cic:/CoRN/tactics/RingReflection/fexprR_mult.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR_mult.con".
 
-inline cic:/CoRN/tactics/RingReflection/fforgetR.con.
+inline "cic:/CoRN/tactics/RingReflection/fforgetR.con".
 
-inline cic:/CoRN/tactics/RingReflection/fexprR2interp.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR2interp.con".
 
-inline cic:/CoRN/tactics/RingReflection/fexprR2wf.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR2wf.con".
 
 (* UNEXPORTED
 Opaque csg_crr.
@@ -142,27 +140,31 @@ Opaque cr_mult.
 Opaque nexp_op.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/refl_interpR.con.
+inline "cic:/CoRN/tactics/RingReflection/refl_interpR.con".
 
-inline cic:/CoRN/tactics/RingReflection/interpR_wd.con.
+inline "cic:/CoRN/tactics/RingReflection/interpR_wd.con".
 
 (* UNEXPORTED
-End Ring_Interpretation_Function.
+End Ring_Interpretation_Function
 *)
 
 (* UNEXPORTED
-Section Ring_NormCorrect.
+Section Ring_NormCorrect
 *)
 
-inline cic:/CoRN/tactics/RingReflection/R.var.
+alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/R.var".
 
-inline cic:/CoRN/tactics/RingReflection/val.var.
+alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/val.var".
 
-inline cic:/CoRN/tactics/RingReflection/unop.var.
+alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/unop.var".
 
-inline cic:/CoRN/tactics/RingReflection/binop.var.
+alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/binop.var".
 
-inline cic:/CoRN/tactics/RingReflection/pfun.var.
+alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/pfun.var".
+
+(* NOTATION
+Notation II := (interpR R val unop binop pfun).
+*)
 
 (*
 four kinds of exprs:
@@ -182,7 +184,7 @@ P: sorted on M, all M's not an I
 Opaque Zmult.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/MI_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/MI_mult_corr_R.con".
 
 (* UNEXPORTED
 Transparent Zmult.
@@ -192,7 +194,7 @@ Transparent Zmult.
 Opaque MI_mult.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/MV_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/MV_mult_corr_R.con".
 
 (* UNEXPORTED
 Transparent MI_mult.
@@ -202,7 +204,7 @@ Transparent MI_mult.
 Opaque MV_mult MI_mult.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/MM_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/MM_mult_corr_R.con".
 
 (* UNEXPORTED
 Transparent MV_mult MI_mult.
@@ -212,7 +214,7 @@ Transparent MV_mult MI_mult.
 Opaque MV_mult.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/MM_plus_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/MM_plus_corr_R.con".
 
 (* UNEXPORTED
 Transparent MV_mult.
@@ -222,7 +224,7 @@ Transparent MV_mult.
 Opaque MM_plus.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con".
 
 (* UNEXPORTED
 Transparent MM_plus.
@@ -232,7 +234,7 @@ Transparent MM_plus.
 Opaque PM_plus.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/PP_plus_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/PP_plus_corr_R.con".
 
 (* UNEXPORTED
 Transparent PM_plus.
@@ -242,13 +244,13 @@ Transparent PM_plus.
 Opaque PM_plus MM_mult MI_mult.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/PM_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/PM_mult_corr_R.con".
 
 (* UNEXPORTED
 Opaque PM_mult.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/PP_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/PP_mult_corr_R.con".
 
 (*
 Transparent PP_plus PM_mult PP_mult PM_plus MI_mult.
@@ -310,12 +312,12 @@ Step_final x2.
 Qed.
 *)
 
-inline cic:/CoRN/tactics/RingReflection/NormR_corr.con.
+inline "cic:/CoRN/tactics/RingReflection/NormR_corr.con".
 
-inline cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con.
+inline "cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con".
 
 (* UNEXPORTED
-End Ring_NormCorrect.
+End Ring_NormCorrect
 *)
 
 (* end hide *)