X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.mli;h=24d5cbc88fd20b6ad1ddda1719473a71ab2353e5;hb=b3e08a6954c8b6946f42f5c7e0bed7912d5ac87c;hp=0ca91fe2c56128549f9789f46aeed4344f72a269;hpb=ed5c4e15429c37bef0f59dfd7160f6883586ed0f;p=helm.git

diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli
index 0ca91fe2c..24d5cbc88 100644
--- a/helm/software/components/tactics/primitiveTactics.mli
+++ b/helm/software/components/tactics/primitiveTactics.mli
@@ -64,6 +64,8 @@ val apply_tac_verbose :
 
 val apply_tac:
   term: Cic.term -> ProofEngineTypes.tactic
+val applyP_tac: (* apply for procedural reconstruction *)
+  term: Cic.term -> ProofEngineTypes.tactic
 val exact_tac:
   term: Cic.term -> ProofEngineTypes.tactic
 val intros_tac: