X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGLocateInductive.ml;h=032060fd3d7d4736f1696188c7cd367a2527911e;hb=36d9dada5eb3894d96c807781e1056b73a1c0a79;hp=04a2f2ad4806f016479dcceb1cafa81d7ceebb75;hpb=506b4b7597021c98e34fb65cf9d0bb7879f06e92;p=helm.git

diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml
index 04a2f2ad4..032060fd3 100644
--- 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