X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Ftactics%2FFieldReflection.ma;h=a3041e0e6354e2081a78d99ac937ff7a919adf42;hb=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;hp=70b61dea5a97b523772a8bb19c4c1a64f3624bdd;hpb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma b/helm/software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma
index 70b61dea5..a3041e0e6 100644
--- a/helm/software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma
@@ -27,18 +27,18 @@ include "algebra/CFields.ma".
 include "tactics/AlgReflection.ma".
 
 (* UNEXPORTED
-Section Field_Interpretation_Function.
+Section Field_Interpretation_Function
 *)
 
-inline "cic:/CoRN/tactics/FieldReflection/F.var".
+alias id "F" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/F.var".
 
-inline "cic:/CoRN/tactics/FieldReflection/val.var".
+alias id "val" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/val.var".
 
-inline "cic:/CoRN/tactics/FieldReflection/unop.var".
+alias id "unop" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/unop.var".
 
-inline "cic:/CoRN/tactics/FieldReflection/binop.var".
+alias id "binop" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/binop.var".
 
-inline "cic:/CoRN/tactics/FieldReflection/pfun.var".
+alias id "pfun" = "cic:/CoRN/tactics/FieldReflection/Field_Interpretation_Function/pfun.var".
 
 inline "cic:/CoRN/tactics/FieldReflection/interpF.ind".
 
@@ -79,22 +79,22 @@ inline "cic:/CoRN/tactics/FieldReflection/refl_interpF.con".
 inline "cic:/CoRN/tactics/FieldReflection/interpF_wd.con".
 
 (* UNEXPORTED
-End Field_Interpretation_Function.
+End Field_Interpretation_Function
 *)
 
 (* UNEXPORTED
-Section Field_NormCorrect.
+Section Field_NormCorrect
 *)
 
-inline "cic:/CoRN/tactics/FieldReflection/F.var".
+alias id "F" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/F.var".
 
-inline "cic:/CoRN/tactics/FieldReflection/val.var".
+alias id "val" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/val.var".
 
-inline "cic:/CoRN/tactics/FieldReflection/unop.var".
+alias id "unop" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/unop.var".
 
-inline "cic:/CoRN/tactics/FieldReflection/binop.var".
+alias id "binop" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/binop.var".
 
-inline "cic:/CoRN/tactics/FieldReflection/pfun.var".
+alias id "pfun" = "cic:/CoRN/tactics/FieldReflection/Field_NormCorrect/pfun.var".
 
 (* NOTATION
 Notation II := (interpF F val unop binop pfun).
@@ -211,7 +211,7 @@ inline "cic:/CoRN/tactics/FieldReflection/Tactic_lemma_zero_F.con".
 inline "cic:/CoRN/tactics/FieldReflection/Tactic_lemmaF.con".
 
 (* UNEXPORTED
-End Field_NormCorrect.
+End Field_NormCorrect
 *)
 
 (* end hide *)