Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics2.mma b/helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics2.mma
index 3352930bec15937b145258747ffdae8273e4e2c6..30fbf96fc7b98fe1b83c7c33881a337dc96f13ac 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics2.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics2.mma
@@ -32,9 +32,9 @@ alias id "b" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Continuity/b.var".
 
 inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_function.ind".
 
-inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_to_pfunct.con".
+inline procedural "cic:/CoRN/tactics/DiffTactics2/cont_to_pfunct.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/DiffTactics2/continuous_cont.con".
+inline procedural "cic:/CoRN/tactics/DiffTactics2/continuous_cont.con" as lemma.
 
 (* UNEXPORTED
 End Automatizing_Continuity
@@ -102,13 +102,13 @@ alias id "b" = "cic:/CoRN/tactics/DiffTactics2/Automatizing_Derivatives/b.var".
 
 inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_function.ind".
 
-inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_to_pfunct.con".
+inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_to_pfunct.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_deriv.con".
+inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_deriv.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_restr.con".
+inline procedural "cic:/CoRN/tactics/DiffTactics2/deriv_restr.con" as lemma.
 
-inline procedural "cic:/CoRN/tactics/DiffTactics2/diffble_restr.con".
+inline procedural "cic:/CoRN/tactics/DiffTactics2/diffble_restr.con" as lemma.
 
 (* UNEXPORTED
 End Automatizing_Derivatives