Pruning candidates in the applicative case for equalities.

[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 cc13d1ad780bf067e7df4ca65ee77ef4bd447ca2..c57efff5d278454bfd65706b31d5062a8c3708ae 100644 (file)
--- a/helm/software/components/tactics/proofEngineHelpers.mli
+++ b/helm/software/components/tactics/proofEngineHelpers.mli
@@ -74,12 +74,13 @@ val pattern_of:
 * *)
 val select:
  metasenv:Cic.metasenv ->
+ subst:Cic.substitution ->
  ugraph:CicUniv.universe_graph ->
  conjecture:Cic.conjecture ->
  pattern:ProofEngineTypes.lazy_pattern ->
   Cic.substitution * Cic.metasenv * CicUniv.universe_graph *
   [ `Decl of (Cic.context * Cic.term) list
-  | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option
+  | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list
   ] option list *
   (Cic.context * Cic.term) list
 
@@ -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 ************************************************)
 
@@ -128,8 +136,3 @@ val split_with_whd: Cic.context * Cic.term ->
                     (Cic.context * Cic.term) list * int
 val split_with_normalize: Cic.context * Cic.term -> 
                           (Cic.context * Cic.term) list * int
-
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
-  * names as long as they are available, then it fallbacks to name generation
-  * using FreshNamesGenerator module *)
-val namer_of: string option list -> ProofEngineTypes.mk_fresh_name_type