(* used only by the old auto *)
val signature_of_goal:
- dbd:HMysql.dbd -> ProofEngineTypes.status ->
+ dbd:HSql.dbd -> ProofEngineTypes.status ->
UriManager.uri list
val signature_of:
MetadataConstraints.UriManagerSet.t
val universe_of_goal:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
bool -> (* apply only or not *)
Cic.metasenv ->
ProofEngineTypes.goal ->
UriManager.uri list
val equations_for_goal:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?signature:MetadataConstraints.term_signature ->
ProofEngineTypes.status -> UriManager.uri list
val experimental_hint:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?facts:bool ->
?signature:MetadataConstraints.term_signature ->
ProofEngineTypes.status ->
(ProofEngineTypes.proof * ProofEngineTypes.goal list))) list
val new_experimental_hint:
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
?facts:bool ->
?signature:MetadataConstraints.term_signature ->
universe:UriManager.uri list ->