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