X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGMatchConclusion.mli;h=a9fbef47fc64a93043228de51855d86dd4817d91;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a8340312f45df33e3b6c3f1a06a3d65f048c11f8;hpb=96134b9ec1030ed15cea00d751dd4d744463f62c;p=helm.git

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.mli b/helm/ocaml/mathql_generator/cGMatchConclusion.mli
index a8340312f..a9fbef47f 100644
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.mli
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.mli
@@ -29,3 +29,5 @@
 val get_constraints: Cic.metasenv -> Cic.context -> Cic.term ->
                      MQGTypes.r_obj list list *  
 		     MQGTypes.r_obj list
+
+val universe       : MQGTypes.universe