Cic.metasenv -> Cic.metasenv -> Cic.context ->
Cic.term -> Cic.term ->
CicUniv.universe_graph ->
- Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+ Subst.substitution * Cic.metasenv * CicUniv.universe_graph
(**
special unification that checks if the two terms are "simple", and in
Cic.metasenv -> Cic.metasenv -> Cic.context ->
Cic.term -> Cic.term ->
CicUniv.universe_graph ->
- Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+ Subst.substitution * Cic.metasenv * CicUniv.universe_graph
(**
searches the library for equalities that can be applied to the current goal
*)
val find_library_equalities:
- HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
+ bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int
(**
val find_context_hypotheses:
Utils.environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
+val get_stats: unit -> string