* *)
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
(* 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 ************************************************)
(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