X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGLocateInductive.mli;h=b6a51401e0805d16cad1a9ea6d1794b9396aa6bf;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e4c6c1fa93badca714d4960f8d304269d22c191d;hpb=506b4b7597021c98e34fb65cf9d0bb7879f06e92;p=helm.git

diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.mli b/helm/ocaml/mathql_generator/cGLocateInductive.mli
index e4c6c1fa9..b6a51401e 100644
--- a/helm/ocaml/mathql_generator/cGLocateInductive.mli
+++ b/helm/ocaml/mathql_generator/cGLocateInductive.mli
@@ -28,6 +28,4 @@
 
 val get_constraints : Cic.term -> MQGTypes.must_restrictions
 
-val universe        : MQGTypes.universe
-
 exception NotAnInductiveDefinition