X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.mli;h=c57efff5d278454bfd65706b31d5062a8c3708ae;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=71486050195dcd55b95961c3c2545e1d304d971f;hpb=36842ee77114d2fa896d7ffd2333c07cff22b053;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index 714860501..c57efff5d 100644
--- a/helm/software/components/tactics/proofEngineHelpers.mli
+++ b/helm/software/components/tactics/proofEngineHelpers.mli
@@ -74,6 +74,7 @@ val pattern_of:
 * *)
 val select:
  metasenv:Cic.metasenv ->
+ subst:Cic.substitution ->
  ugraph:CicUniv.universe_graph ->
  conjecture:Cic.conjecture ->
  pattern:ProofEngineTypes.lazy_pattern ->