X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGMatchConclusion.mli;h=a9fbef47fc64a93043228de51855d86dd4817d91;hb=506b4b7597021c98e34fb65cf9d0bb7879f06e92;hp=a8340312f45df33e3b6c3f1a06a3d65f048c11f8;hpb=962cc970cd9a2161f69b70aa01b6ee9e289d9778;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