Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics3.mma b/helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics3.mma
index 3e2b4f152243aa4fe7285df5d86cf5595406549b..01be53402db91754ca68a42499031fc6c69f23b8 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics3.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/tactics/DiffTactics3.mma
@@ -43,9 +43,9 @@ inline procedural "cic:/CoRN/tactics/DiffTactics3/symbPF.ind".
   | ssum      : nat->nat->(nat->symbPF)->symbPF
 *)
 
-inline procedural "cic:/CoRN/tactics/DiffTactics3/symb_to_PartIR.con".
+inline procedural "cic:/CoRN/tactics/DiffTactics3/symb_to_PartIR.con" as definition.
 
-inline procedural "cic:/CoRN/tactics/DiffTactics3/symbPF_deriv.con".
+inline procedural "cic:/CoRN/tactics/DiffTactics3/symbPF_deriv.con" as definition.
 
 (* UNEXPORTED
 Ltac PartIR_to_symbPF f :=