cicDischarge: new module for discharging the explicit variables occurring in a

[helm.git] / helm / software / components / tactics / proofEngineHelpers.mli

diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index a51213f9377635aa5a4d8dacde53eedb9976f67c..71486050195dcd55b95961c3c2545e1d304d971f 100644 (file)
--- a/helm/software/components/tactics/proofEngineHelpers.mli
+++ b/helm/software/components/tactics/proofEngineHelpers.mli
@@ -109,6 +109,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 ************************************************)