X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FfreshNamesGenerator.ml;h=fbb90552aa9e4293792743a3329e248c9b24ae90;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=3bdde5b593426125143aa874e904feb1069d1e4b;hpb=a785a3526d4dcbb6c5810ed4fb943132c9ff2d45;p=helm.git

diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml
index 3bdde5b59..fbb90552a 100644
--- a/helm/ocaml/cic_unification/freshNamesGenerator.ml
+++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml
@@ -34,7 +34,10 @@ let mk_fresh_name ~subst metasenv context name ~typ =
       C.Anonymous ->
        (*CSC: great space for improvements here *)
        (try
-         (match CicTypeChecker.type_of_aux' ~subst metasenv context typ with
+        let ty,_ = 
+          CicTypeChecker.type_of_aux' ~subst metasenv context typ 
+            CicUniv.empty_ugraph in 
+         (match ty with
              C.Sort C.Prop
            | C.Sort C.CProp -> "H"
            | C.Sort C.Set -> "x"