CGLocateInductive patched

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

diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml
index 04a2f2ad4806f016479dcceb1cafa81d7ceebb75..032060fd3d7d4736f1696188c7cd367a2527911e 100644 (file)
--- a/helm/ocaml/mathql_generator/cGLocateInductive.ml
+++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml
@@ -38,5 +38,3 @@ let get_constraints = function
       let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in
       (constr_obj, constr_rel, constr_sort)
    | _                      -> raise NotAnInductiveDefinition
-
-let universe = CGSearchPattern.universe