...

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma b/helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma
index 4a348ceae7b6a946b8d5023ff6bc40236406154f..d51f1688706acd4ebebc511ee4359160985165d7 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/tactics/RingReflection.mma
@@ -28,15 +28,25 @@ include "tactics/AlgReflection.ma".
 Section Ring_Interpretation_Function
 *)
 
-alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/R.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/R.var
+*)
 
-alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/val.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/val.var
+*)
 
-alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/unop.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/unop.var
+*)
 
-alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/binop.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/binop.var
+*)
 
-alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/pfun.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/pfun.var
+*)
 
 inline procedural "cic:/CoRN/tactics/RingReflection/interpR.ind".
 
@@ -150,15 +160,25 @@ End Ring_Interpretation_Function
 Section Ring_NormCorrect
 *)
 
-alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/R.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/R.var
+*)
 
-alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/val.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/val.var
+*)
 
-alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/unop.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/unop.var
+*)
 
-alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/binop.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/binop.var
+*)
 
-alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/pfun.var".
+(* UNEXPORTED
+cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/pfun.var
+*)
 
 (* NOTATION
 Notation II := (interpR R val unop binop pfun).