(* used only by the old auto *)
val signature_of_goal:
- dbd:HMysql.dbd -> ProofEngineTypes.status ->
+ dbd:HSql.dbd -> ProofEngineTypes.status ->
UriManager.uri list
-val universe_of_goals:
- dbd:HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
+val signature_of:
+ Cic.metasenv ->
+ ProofEngineTypes.goal ->
+ MetadataConstraints.UriManagerSet.t
+
+val signature_of_hypothesis:
+ Cic.hypothesis list ->
+ Cic.metasenv ->
+ MetadataConstraints.UriManagerSet.t
+
+val close_with_types:
+ MetadataConstraints.UriManagerSet.t ->
+ Cic.metasenv ->
+ Cic.context ->
+ MetadataConstraints.UriManagerSet.t
+
+val universe_of_goal:
+ 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 ->