X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcontribs%2FCoRN-Decl%2Ftactics%2FRingReflection.ma;h=84a076ad99d28cb5c0ebe3eab29cfdbf71a3db6d;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=c4d87d25105a3c523e458610043a6eee84a72d9e;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git

diff --git a/matita/contribs/CoRN-Decl/tactics/RingReflection.ma b/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
index c4d87d251..84a076ad9 100644
--- a/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
+++ b/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
@@ -27,18 +27,18 @@ include "algebra/CRings.ma".
 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".
 
@@ -145,22 +145,26 @@ inline "cic:/CoRN/tactics/RingReflection/refl_interpR.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:
@@ -313,7 +317,7 @@ inline "cic:/CoRN/tactics/RingReflection/NormR_corr.con".
 inline "cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con".
 
 (* UNEXPORTED
-End Ring_NormCorrect.
+End Ring_NormCorrect
 *)
 
 (* end hide *)