added the support for the "Locate Inductive Principles" query

[helm.git] / helm / ocaml / mathql_generator / cGSearchPattern.ml

diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml
index 60633f897e722f988990d7157506ce178b052e34..77f3b488c6e896a7285e3ef2a0c73e2f415f87d9 100644 (file)
--- a/helm/ocaml/mathql_generator/cGSearchPattern.ml
+++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml
@@ -187,3 +187,6 @@ let get_constraints term =
    ) sorts ;
   res
 ;;
+
+let universe =
+   [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]