X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fmathql_generator%2FcGSearchPattern.ml;h=77f3b488c6e896a7285e3ef2a0c73e2f415f87d9;hb=c172220b965a4d0e95004ae42911a886faac878c;hp=60633f897e722f988990d7157506ce178b052e34;hpb=96134b9ec1030ed15cea00d751dd4d744463f62c;p=helm.git diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml index 60633f897..77f3b488c 100644 --- 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]