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