| 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 :=