* subterms of the conclusion with their context. Note: in the result the list
* of hypotheses * has an entry for each entry in the context and in the same
* order. Of course the list of terms (with their context) associated to one
-* hypothesis may be empty. *)
+* hypothesis may be empty.
+*
+* @raise Bad_pattern
+* *)
val select:
metasenv:Cic.metasenv ->
ugraph:CicUniv.universe_graph ->