X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.mli;h=c57efff5d278454bfd65706b31d5062a8c3708ae;hb=765eb07cafb8a06a5027f4569ad06d805aba2488;hp=a51213f9377635aa5a4d8dacde53eedb9976f67c;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index a51213f93..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 ->
@@ -109,6 +110,13 @@ val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
 (* orders a metasenv w.r.t. dependency among metas *)
 val sort_metasenv: Cic.metasenv -> Cic.metasenv
 
+(* finds an hypothesis by name in the context *)
+val find_hyp: string -> Cic.context -> Cic.term * Cic.term
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+val sort_pattern_hyps:
+ Cic.context -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.lazy_pattern
+
 
 (* FG: some helper functions ************************************************)