let set_main_position pos depth = match pos with
| `MainHypothesis _ -> `MainHypothesis depth
| `MainConclusion _ -> `MainConclusion depth
-
-let universe_for_search_pattern =
- [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]
-
-let universe_for_match_conclusion = [T.MainConclusion; T.InConclusion]